7 ms·

The great thing about state machines is that they are easy to debug. Once you have co-routines firing off co-routines, you're in co-routine spaghetti. In fact,

The great thing about state machines is that they are easy to debug. Once you have co-routines firing off co-routines, you're in co-routine spaghetti. In fact, I'll coin the term now: co-routines = "asynchronous gotos".

eliben 12y ago
Can you clarify why state machines are easier to debug?
- hadoukenio 12y ago
  I've worked on large state machines in the past, which were rock solid and easy to work with. As the code was built using state transition tables, state machines were automatic. I would hate to think of how to juggle these systems using co-routines.
  - eliben 12y ago
    I'm not sure you're answering my question, though. You made a claim that state machines are easy to debug and coroutines are not. What makes you think they are not? I'm really just curious. FWIW I've done significanly more work with state machines in the past, and I find them reasonable to debug, though not as easy as straight line code because in the latter the full state history (execution stack) is always known, while in state machines you usually need to do extra work to trace how the machine got to some state.
    - hadoukenio 12y ago
      Sorry I forgot my why. Probably because by using state transition tables the system's whereabouts is afforded salience. Compare this to a co-routines being sprinkled throughout a large code base, essentially creating asynchronous goto-hell.
    - deleted 12y ago
      [deleted]
- xsmasher 12y ago
  When I'm writing a state machine I make sure to add a method like machine.changeState( newState, "reason"); Now you can add a dlog inside changeState to see a history of state transitions and why they were made; useful for figuring out why you got where. That's not something inherent to state machines, though.
- lmm 12y ago
  An explicit state machine makes it very easy to observe a) what the current state is b) what the possible states are.
tlarkworthy 12y ago
I wrote a state machine abstraction for Firebase [1], then implemented cross tree transactions on top, which was the formally verified to be exploit free. I think co-routines are a bit too general to make formal verification straight forward. [1] http://tomlarkworthy.github.io/ http://tomlarkworthy.github.io/
- erichocean 12y ago
  That is a seriously cool project! I wish more people took advantage of both HSMs and theorem provers, and you've done both. Nice. :)
  - tlarkworthy 12y ago
    thanks a lot. Yeah, its a brutal bug exterminator combo, and somewhat easier to wrap your head around that coq or similar. I am trying to find an organic use of the H in HSM for server side stuff, but struggling to think of examples that are not contrived if you have any.
- oggy 12y ago
  That looks cool. Could you explain a bit more about how the formal verification part worked? What kind of prover do you use? Are the HSMs the specification, and you want to make sure that the rules behave as specified by the HSMs, or do you specify some higher level properties on the HSMs? I couldn't figure these out scanning through your website.
  - tlarkworthy 12y ago
    The HSMs are converted to Firebase security rules. The theorem proover is used to verify somewhat arbitrary higher level properties So for item trade* I was specifying the that no new items could be introduced (dupe bugs) or removed from the system, and that a player could never get stuck in a state they could never leave (deadlock). The HSM abstraction is just a useful notation for developing such protocols, though the formal verification actually operated on the Firebase security rule level. * https://github.com/tomlarkworthy/firesafe/wiki/Send-Item https://github.com/tomlarkworthy/firesafe/wiki/Send-Item EDIT: reply to oggy's child question as I can't reply underneath. The actual spec prooving bit is secret sauce territory until I work out what the future holds for this project.
jeremiep 12y ago
Debugging ease is highly dependant on the implementation of either state machines or co-routines, especially if there are heavy compile-time transformations of the code structure involved. In either case, if the implementation supports the composition of state machines or co-routines, its going to be easy to reason about.

eliben 12y ago

Can you clarify why state machines are easier to debug?

hadoukenio 12y ago
I've worked on large state machines in the past, which were rock solid and easy to work with. As the code was built using state transition tables, state machines were automatic. I would hate to think of how to juggle these systems using co-routines.
- eliben 12y ago
  I'm not sure you're answering my question, though. You made a claim that state machines are easy to debug and coroutines are not. What makes you think they are not? I'm really just curious. FWIW I've done significanly more work with state machines in the past, and I find them reasonable to debug, though not as easy as straight line code because in the latter the full state history (execution stack) is always known, while in state machines you usually need to do extra work to trace how the machine got to some state.
  - hadoukenio 12y ago
    Sorry I forgot my why. Probably because by using state transition tables the system's whereabouts is afforded salience. Compare this to a co-routines being sprinkled throughout a large code base, essentially creating asynchronous goto-hell.
  - deleted 12y ago
    [deleted]
xsmasher 12y ago
When I'm writing a state machine I make sure to add a method like machine.changeState( newState, "reason"); Now you can add a dlog inside changeState to see a history of state transitions and why they were made; useful for figuring out why you got where. That's not something inherent to state machines, though.
lmm 12y ago
An explicit state machine makes it very easy to observe a) what the current state is b) what the possible states are.

tlarkworthy 12y ago

I wrote a state machine abstraction for Firebase [1], then implemented cross tree transactions on top, which was the formally verified to be exploit free. I think co-routines are a bit too general to make formal verification straight forward. [1] http://tomlarkworthy.github.io/ http://tomlarkworthy.github.io/

erichocean 12y ago
That is a seriously cool project! I wish more people took advantage of both HSMs and theorem provers, and you've done both. Nice. :)
- tlarkworthy 12y ago
  thanks a lot. Yeah, its a brutal bug exterminator combo, and somewhat easier to wrap your head around that coq or similar. I am trying to find an organic use of the H in HSM for server side stuff, but struggling to think of examples that are not contrived if you have any.
oggy 12y ago
That looks cool. Could you explain a bit more about how the formal verification part worked? What kind of prover do you use? Are the HSMs the specification, and you want to make sure that the rules behave as specified by the HSMs, or do you specify some higher level properties on the HSMs? I couldn't figure these out scanning through your website.
- tlarkworthy 12y ago
  The HSMs are converted to Firebase security rules. The theorem proover is used to verify somewhat arbitrary higher level properties So for item trade* I was specifying the that no new items could be introduced (dupe bugs) or removed from the system, and that a player could never get stuck in a state they could never leave (deadlock). The HSM abstraction is just a useful notation for developing such protocols, though the formal verification actually operated on the Firebase security rule level. * https://github.com/tomlarkworthy/firesafe/wiki/Send-Item https://github.com/tomlarkworthy/firesafe/wiki/Send-Item EDIT: reply to oggy's child question as I can't reply underneath. The actual spec prooving bit is secret sauce territory until I work out what the future holds for this project.

jeremiep 12y ago

Debugging ease is highly dependant on the implementation of either state machines or co-routines, especially if there are heavy compile-time transformations of the code structure involved. In either case, if the implementation supports the composition of state machines or co-routines, its going to be easy to reason about.