3 ms·

> The TLA+ model basically pointed out that the (finite sized) message buffer can grow without bounds if notifications are missed over and over (e.g. a super sh

> The TLA+ model basically pointed out that the (finite sized) message buffer can grow without bounds if notifications are missed over and over (e.g. a super shitty RF environment). I've got a strategy that might work for polling it periodically, but I don't know that I would have realized this failure path without modelling it. Obviously I don't know anything about your use case, and I apologize if this comes across as unsolicited advice, but this sounds like a pretty textbook example of a situation where load shedding is your only option -- even if you manage to figure out the polling problems.

tonyarkles 7y ago
Oh, the device itself keeps a finite-sized mailbox and deletes the oldest message if it's full. The concern is that one of the deleted messages might have been important (e.g. informing us that a transmission failed, or informing us that Search & Rescue got the message and is sending a helicopter). The polling is a backup plan that at least gives the phone feedback if it's not working (a failed read informs the phone that the read failed; a failed notification doesn't tell either side that something failed). We can still obviously lose messages if enough of them come in between polling intervals, but it's better than potentially losing messages indefinitely without knowing about it. The other nice thing is that we can keep metrics for how often the polling process actually finds things that we weren't successfully notified about. That'll either give us leverage to encourage the vendor to switch to indications instead of notifications, or encourage us to find a new vendor :) Edit: and yes, I 100% appreciate the feedback!
- QuinnWilton 7y ago
  That makes a lot of sense! Thanks for elaborating :) If you don't mind me asking, what are you working on / what is your background? It sounds like you're doing a ton of really interesting engineering, involving a lot of moving parts.
  - tonyarkles 7y ago
    I don't mind at all! It'll be like a tiny advertisement for my consulting company. For undergrad, my school didn't have a Computer Engineering program, so I did EE and a special CS program they had for engineers (all of the CS and Math credits of a 4-year CS degree, none of the arts electives). In EE, I focused primarily on small-signal stuff (DSP, Digital Communications, Control Systems, HDL, etc), and in CS I basically drank from the fire hose (my 4th year electives were Security, Compiler Design, Advanced Algorithms, and OS Concepts 2). I went and worked for a few years, first at a startup doing electronic design software, and then at a "hot web company". Got a bit bored, went back and did an M.Sc. in Comp Sci, focused on Distributed Systems (my thesis was basically New Relic before that was a thing...) About 18 months into grad school, my funding ran out. Coincidentally, a friend showed up and asked me if I wanted to do some backend programming for a side gig he'd picked up. That turned into he and I going full-time running a web/mobile company for a few years. Made decent money at that, rode the "mobile is the new hotness" wave, but wasn't feeling super fulfilled. He ended up moving across the country, and we broke up the company. With my newfound freedom, I started shifting away from web/mobile stuff as much as I could and focusing more on lower-level type work (put that EE degree to use!). I don't really have a portfolio put together, but here's a few examples of the cool projects; remember that this is like a person's social media feed and it's the highlights. There's been boring projects as well, and there's been a month here and there with no income at all. - GNSS satellite simulator for testing GNSS receivers. We simulated the orbits of entire constellations of GNSS satellites with ~1m precision, simulated the signals they were transmitting and the delays those signals would experience (due to distance and atmospheric interference), and put the combined output into a Software-Defined Radio. Good enough to convince the receivers I tested with! This had a bunch of C code for doing the simulation and signal generation, and a Python scripting interface on top. - Live animation/Motion Capture. Took a handful of 1st-gen Kinects, put them on tripods, and turned them into an "all aspect ratio" motion capture system that didn't require special suits/rooms/tags. After putting them around the room, they would auto-calibrate themselves to figure out where they were relative to each other, and then spit out a stream of joint positions in a world frame. This got streamed into... maybe it was 3DS Max? Either way, the joint positions and angles were mapped onto a live model. - The ill-fated Peachy Printer (if you missed the drama, I'm pretty sure it's still online somewhere). UV laser- and resin-based dirt cheap 3D printer. I ended up in the right place at the right time and ended up designing the digital version of the main PCB (first version plugged into your sound card, my version was USB). - A fuel-monitoring system that keeps track of tank farms all over Western Canada. I didn't make this hardware, but significantly rewrote a bunch of the software for performance reasons, and added robust networking to it. From the central office, you can see how much fuel is in every tank across 3 provinces and make scheduling/routing decisions. (These are the 80,000L tanks you see on the side of the road in rural areas). - A giant hexcopter for agriculture. This is still a work in progress but testing is suspended until spring when there's more than just a thick layer of snow on the ground. I mostly worked on the mechanical design and the flight controller, with a bit of input here and there for the payload and other electronics. - A Bluetooth personal safety device. When I joined the project, a 3rd-party had designed and manufactured the hardware; a different 3rd-party had designed the mobile apps. Everything was pretty flaky. I did a bit of firmware work on the device itself, and a significant rewrite of the Android Bluetooth code to make it drastically more reliable. This is the same company that is now integrating with the BLE-Iridium device to be able to provide coverage out of cell range. The coolest part of this project? There are people who are alive because of this project, and who likely would have died if the code was bad. - A clean-sheet implementation of the LoRaWAN protocol. A client looked at the reference library provided by Semtech and felt they couldn't rely on the code. I made up the TLA+ model based on the spec (and uhh deviations from the spec that we learned about in certain hardware), and iterated on the spec until it seemed robust. "Ported" it from TLA+ to C, and it worked like a hot-damn. Thanks for asking about this, by the way... I'm going to save this post as a bit of a resume and iterate on it to figure out what I've missed! p.s. I love the website.

tonyarkles 7y ago

Oh, the device itself keeps a finite-sized mailbox and deletes the oldest message if it's full. The concern is that one of the deleted messages might have been important (e.g. informing us that a transmission failed, or informing us that Search & Rescue got the message and is sending a helicopter). The polling is a backup plan that at least gives the phone feedback if it's not working (a failed read informs the phone that the read failed; a failed notification doesn't tell either side that something failed). We can still obviously lose messages if enough of them come in between polling intervals, but it's better than potentially losing messages indefinitely without knowing about it. The other nice thing is that we can keep metrics for how often the polling process actually finds things that we weren't successfully notified about. That'll either give us leverage to encourage the vendor to switch to indications instead of notifications, or encourage us to find a new vendor :) Edit: and yes, I 100% appreciate the feedback!

QuinnWilton 7y ago
That makes a lot of sense! Thanks for elaborating :) If you don't mind me asking, what are you working on / what is your background? It sounds like you're doing a ton of really interesting engineering, involving a lot of moving parts.
- tonyarkles 7y ago
  I don't mind at all! It'll be like a tiny advertisement for my consulting company. For undergrad, my school didn't have a Computer Engineering program, so I did EE and a special CS program they had for engineers (all of the CS and Math credits of a 4-year CS degree, none of the arts electives). In EE, I focused primarily on small-signal stuff (DSP, Digital Communications, Control Systems, HDL, etc), and in CS I basically drank from the fire hose (my 4th year electives were Security, Compiler Design, Advanced Algorithms, and OS Concepts 2). I went and worked for a few years, first at a startup doing electronic design software, and then at a "hot web company". Got a bit bored, went back and did an M.Sc. in Comp Sci, focused on Distributed Systems (my thesis was basically New Relic before that was a thing...) About 18 months into grad school, my funding ran out. Coincidentally, a friend showed up and asked me if I wanted to do some backend programming for a side gig he'd picked up. That turned into he and I going full-time running a web/mobile company for a few years. Made decent money at that, rode the "mobile is the new hotness" wave, but wasn't feeling super fulfilled. He ended up moving across the country, and we broke up the company. With my newfound freedom, I started shifting away from web/mobile stuff as much as I could and focusing more on lower-level type work (put that EE degree to use!). I don't really have a portfolio put together, but here's a few examples of the cool projects; remember that this is like a person's social media feed and it's the highlights. There's been boring projects as well, and there's been a month here and there with no income at all. - GNSS satellite simulator for testing GNSS receivers. We simulated the orbits of entire constellations of GNSS satellites with ~1m precision, simulated the signals they were transmitting and the delays those signals would experience (due to distance and atmospheric interference), and put the combined output into a Software-Defined Radio. Good enough to convince the receivers I tested with! This had a bunch of C code for doing the simulation and signal generation, and a Python scripting interface on top. - Live animation/Motion Capture. Took a handful of 1st-gen Kinects, put them on tripods, and turned them into an "all aspect ratio" motion capture system that didn't require special suits/rooms/tags. After putting them around the room, they would auto-calibrate themselves to figure out where they were relative to each other, and then spit out a stream of joint positions in a world frame. This got streamed into... maybe it was 3DS Max? Either way, the joint positions and angles were mapped onto a live model. - The ill-fated Peachy Printer (if you missed the drama, I'm pretty sure it's still online somewhere). UV laser- and resin-based dirt cheap 3D printer. I ended up in the right place at the right time and ended up designing the digital version of the main PCB (first version plugged into your sound card, my version was USB). - A fuel-monitoring system that keeps track of tank farms all over Western Canada. I didn't make this hardware, but significantly rewrote a bunch of the software for performance reasons, and added robust networking to it. From the central office, you can see how much fuel is in every tank across 3 provinces and make scheduling/routing decisions. (These are the 80,000L tanks you see on the side of the road in rural areas). - A giant hexcopter for agriculture. This is still a work in progress but testing is suspended until spring when there's more than just a thick layer of snow on the ground. I mostly worked on the mechanical design and the flight controller, with a bit of input here and there for the payload and other electronics. - A Bluetooth personal safety device. When I joined the project, a 3rd-party had designed and manufactured the hardware; a different 3rd-party had designed the mobile apps. Everything was pretty flaky. I did a bit of firmware work on the device itself, and a significant rewrite of the Android Bluetooth code to make it drastically more reliable. This is the same company that is now integrating with the BLE-Iridium device to be able to provide coverage out of cell range. The coolest part of this project? There are people who are alive because of this project, and who likely would have died if the code was bad. - A clean-sheet implementation of the LoRaWAN protocol. A client looked at the reference library provided by Semtech and felt they couldn't rely on the code. I made up the TLA+ model based on the spec (and uhh deviations from the spec that we learned about in certain hardware), and iterated on the spec until it seemed robust. "Ported" it from TLA+ to C, and it worked like a hot-damn. Thanks for asking about this, by the way... I'm going to save this post as a bit of a resume and iterate on it to figure out what I've missed! p.s. I love the website.