How to Replay a State Machine in a Debugger

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:

• tui-rs
• Crossterm
• The reedline crate
• Episode about the "Sidecar" switch
• Elm time-travel debugging
• Replay.io
• Devtools.fm episode on Replay.io
• AADEBUG conference
• California horse meat law

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 rese...