Back
S03 E09
27 Mar 2023/01:08:22

Get You a State Machine for Great Good

Andrew Stone of Oxide Engineering joined Bryan, Adam, and the Oxide Friends to talk about his purpose-built, replay debugger for the Oxide setup textual UI. Andrew borrowed a technique from his extensive work with distributed systems to built a UI that was well-structured... and highly amenable to debuggability. He built a custom debugger "in a weekend"!

Some of the topics we hit on, in the order that we hit them:
The (lightly) edited live chat from the show:
  • MattCampbell: I'm gathering that this is more like the fancy pseudo-GUI style of TUI, which is possibly bad for accessibility
  • ahl: we are also building with accessibility in mind, stripping away some of the non-textual elements optionally
  • MattCampbell: oh, cool
  • ahl: Episode about the "Sidecar" switch: https://github.com/oxidecomputer/oxide-and-friends/blob/master/2021_11_29.md
  • MattCampbell: ooh! That kind of recording is definitely better for accessibility than a video.
  • uwaces: Were you inspired by Elm? (The programming language for web browsers?)
  • bcantrill: Here's Andrew's PR for this, FWIW: oxidecomputer/omicron#2682
  • uwaces: Elm has a very similar model. They have even had a debugger that let you run events in reverse: https://elm-lang.org/news/time-travel-made-easy
  • bch: I’m joining late - 1) does this state-machine replay model have a name 2) expand on (describe ) the I/o logic separation distinction?
  • ahl: http://dtrace.org/blogs/ahl/2015/06/22/first-rust-program-pain/
  • zk: RE: logic separation in consensus protocols: the benefit of seperating out the state machine into a side-effect free function allows you to write a formally verified implementation in a pure FP lang or theorem prover, and then extract a reference program from the proof.
  • we're going to the zoo: lol i’m a web dev && we do UI tests via StorybookJS + snapshots of each story + snapshots of the end state of an interaction
  • ig: At that point you could turn the recording into an “expect test”. https://blog.janestreet.com/the-joy-of-expect-tests/
  • we're going to the zoo: TOFU but for tests 🥰
  • uwaces: Are you at all worried that you are replicating the horror that is the IBM 3270 terminal? — I have personal history programming on z/OS where the only interface is a graphical EBCDIC 3027 interface — the horror is that people write programs to interact with graphical window (assuming a certain size).
  • ahl: https://docs.rs/serde/latest/serde/#data-formats
  • ahl: SHOW NOTES Bryan as "semi-elderly" engineer
  • MattCampbell: didn't Bryan write a blog post on this?
  • MattCampbell: http://dtrace.org/blogs/bmc/2008/11/16/on-modalities-and-misadventures/
  • uwaces: https://www.replay.io
  • ahl: https://devtools.fm/episode/9
  • ahl: e.g. https://altsysrq.github.io/proptest-book/intro.html
  • we're going to the zoo: https://github.com/AFLplusplus/LibAFL
  • ig: Are you using proptest, quickcheck, or something else?
  • nickik: This really started with Haskell https://hackage.haskell.org/package/QuickCheck Its also cool that it does 'narrowing' meaning it will try to find an error, and then try to generate a simpler error case.
  • endigma: how different is something like this from what go calls "fuzzing"
  • Riking: Fuzzing does also have a minimization step
  • we're going to the zoo: https://github.com/dubzzz/fast-check
  • Riking: Property-based testing tends to be structured differently in philosophy, while fuzzers are more aligned to "give you a bag of bytes"
  • nickik: http://www.quviq.com/products/erlang-quickcheck/
  • endigma: yeah I can tell its a different structure, but the overall goal seems similar
  • we're going to the zoo: they are nonexclusive approaches to testing
  • papertigers: I think Kelly was doing a bunch of tests at Joyent based on quick check and prop test. First time I encountered it
  • we're going to the zoo: libafl provides a #[derive(Arbitrary)] macro that will provide the correct values for a struct
  • uwaces: Lots of stuff in Rust existed first in Haskell (build.rs, quote!, Derive macros, Traits, ect….)…
  • nixinator: https://tenor.com/view/%C3%B3culos-escuro-exterminador-terminator-arnold-schwarzenegger-gif-14440790
  • we're going to the zoo: “what do these means” depends on who you ask lol
  • we're going to the zoo: fast-check is 🔥 for TypeScript
  • endigma: if the tested function is deterministic and the test is testing arbitrary input and testing against the result to be derivative in some way of the input function by some f(x), don't you end up re-implementing the tested function to provide the expected result? how does the author choose what properties of a system to test without falling into a "testing the test" pit?
  • we're going to the zoo: Rust: “Here comes the Haskell plane!”
  • nixinator: Isn’t rust == oxidation
  • endigma: yes
  • endigma: in a scientific sense
  • nixinator: Iron oxide 🙂 lol
  • nixinator: Very good!
  • GeneralShaw: Is prop test a way of formal verification? Is it same/different?
  • ahl: https://dl.acm.org/conference/aadebug
  • ig: I mean, Haskell is an academic research language at it’s core. It naturally is going to try new things and try and push the envelope, that’s what many of the core developers use the language for.
  • uwaces: Not all of the Haskell ideas are good :). Rusts thesis when it started was “let’s take the good boring ideas that are >20 years old and leave the exciting new ones out”. Haskell is all about the exciting new ideas that might be bad (Lenes, lazy evaluation, ect…)
  • ig: Rust had Servo as it’s driving force in the early stages as well, so was choosing features that made implementing Servo easier.
  • endigma: the parallel between haskell and elixir is interesting, elixir being "the other functional language" that exists in the sort of limelight
  • nickik: Not really, formal verification proves that it satisfied some condition, property based testing basically just throws a bunch of stuff against your code and tries to break it.
  • ElFurbe: "score some horse"
  • ElFurbe: Outstanding
  • nickik: In Switzerland at least horse meat is totally normal, just buy it in a standard boring store.
  • rolypoly: Ballmer curve, but with horse, and for debugging.
  • uwaces: On that topic Rust has some exciting usability developments for Bounded model checking: https://github.com/model-checking/kani — proving correctness of property tests.
  • ig: Okay I tuned out for a minute and now I’m wondering if I’m having a fever dream.
  • GeneralShaw: Oh that sounds like Constrained random tests, but somehow takes the properties as the constraints
  • endigma: debugging -> stroke -> horse meat
  • nickik: Good horse: https://www.migros.ch/de/product/mo/3851110
  • Nahum: The word he was looking for was probably "elder"
  • ig: Event sourcing is also in that same CQRS family.
  • ig: In terms of google able terms
  • endigma: isn't cqrs command query separation
  • ig: Event sourcing becomes harder when you need to do GDPR right to amend and right to be forgotten.
  • uwaces: Yay for struct opt!
  • ig: Thanks Andrew! Great episode.
  • nickik: Datomic style databases allows you to have traditional-ish database but you can also subscribe to the event log. To comply with GDPR you can use 'Excision'. That will delete the data but it remember the transaction that did the removal.
  • endigma: Datomic looks really interesting, never heard of this style of db before, sort of like the git db
  • ig: Yeah, and if you didn’t build that in from the start you might end up needing an O(n) processing of the event log to excise.
  • ajs: Kani looks super interesting
  • ajs: I've had it on the backlog to play with for a while
  • ig: Most DBs have a commit log, most don’t expose it externally. Event sourcing reimplements a lot of what’s in the commit log.
  • nickik: Maybe more practical then full datomic, datascript (https://github.com/tonsky/datascript) is datomic in a browser. Good store for React applications to build on.
  • nickik: Eventsourcing can scale to much larger size then you can handle with one Datomic style DB. But unless you really need it, its kind of a pain.
  • endigma: is there anything preventing implementing it as a data structure ontop of a more conventional db?
  • nickik: Datomic allows you to add arbitrary data to your transactional log, so for example you can attach to a transaction that it was done by user-x, threw api versions 2.2 and so on. That quite neat.
  • nickik: That's exactly what datomic does, its designed to be read-scalable on big key value stores, but it works fine on SQL Databases! See: https://docs.datomic.com/on-prem/overview/storage.html
  • endigma: oh thats pretty cool, i suppose the datom model would work well with hyperscale k/v
  • endigma: from what i'm reading datoms are a sort of tuple though, k/v doesn't normally index by more than one k
  • endigma: i wonder how batching lookups works to get the k/v of a particular entity
  • endigma: or if they all just happen separately and its optimized for that
  • endigma: Although I'm thinking like etcd
  • uwaces: No. It just automates example creation. The same general framework can be used to do formal verification re:Kani and bounded model checking.
  • Cyborus: ah, it seems i'm a bit late
  • nickik: It does not use the K/V store directly. It puts large batches into one V. Then the have an external index that is a bunch of trees and the leafs are these batches of datoms. This has some information: https://tonsky.me/blog/unofficial-guide-to-datomic-internals/ or check out Rick Hickeys talks on YT.
  • endigma: Sure, so more similar to the goal of fuzz tests than unit tests.
  • we're going to the zoo: https://www.bjaress.com/posts/2021-07-03-fuzz-testing-vs-property-based-testing.html a reasonable approach will use both a naive and structured generative test
  • we're going to the zoo: a fuzz test is just a property test that claims “for any possible input, the program should only output the types i expect / a known exception”
  • endigma: if thats correct it makes a lot of sense why you might want to make a framework to write these sort of assumptions, perhaps something like go-testdeep
  • endigma: (sort of)
  • endigma: https://earthly.dev/blog/property-based-testing/
If we got something wrong or missed something, please file a PR! Our next show will likely be on Monday at 5p Pacific Time on our Discord server; stay tuned to our Mastodon feeds for details, or subscribe to this calendar. We'd love to have you join us, as we always love to hear from new speakers!

Give feedback