Elektrine lite

← Feed

@lindsey@recurse.social

Post #1657065

2026-04-23 21:27 UTC

Just got owned by a student who pointed out that a distributed snapshot algorithm that does nothing, takes an empty snapshot, and terminates immediately is both safe and live according to the safety (doesn't take inconsistent snapshots) and liveness (terminates) criteria I had written down.

Replies (6)

  • @lindsey@recurse.social 2026-04-23 21:28

    I guess we also need some sort of non-triviality criterion like "doesn't always produce the same snapshot", kind of like how the validity criterion for consensus algorithms rules out algorithms that ignore their input and always decide on the same value

    Open ##1823370

  • @dpk@chaos.social 2026-04-23 21:32

    @lindsey There should be a meta-law of mathematics that says when you think you found a dichotomy, it’s probably a ‘pick two of three’ but you forgot the third because it seems too trivial to consider

    Open ##1823392

  • @jrose@social.belkadan.com 2026-04-23 21:32

    @lindsey Reminds me of an (internal) presentation about zero-knowledge proofs where the presenter showed an example system that is successfully zero-knowledge but does not actually prove anything.

    Open ##1823403

  • @cigitalgem@sigmoid.social 2026-04-23 21:55

    @lindsey time stamp

    Open ##1823404

  • @dpiponi@mathstodon.xyz 2026-04-23 21:59

    @lindsey When I was reading papers on distributed systems there were a bunch of times things like this seemed to come up. I was never sure if it was because I missed some clause in the text, or if I simply misunderstood. I did sometimes think about the third option but it's harder to read papers when you relax the assumption they're correct :)

    Open ##1823405

  • @lindsey reminds me of the one weird trick for designing an operational semantics that is type-sound and strongly normalising (do nothing).

    Open ##1823409