[docs] State machine event handler semantics: atomic execution?

[oberstet]

I've been trying to figure out the semantics of state machine event handlers: are state machine event handlers executed atomically once triggered?

IOW: does P create new state sequences within the execution of an event handler, or are new state sequences only introduced when a new event is processed (received) or a message is sent?

The docs in

https://p-org.github.io/P/manual/statemachines/
https://p-org.github.io/P/advanced/psemantics/

say

Each state in the P state machine has an entry function associated with it which gets executed when the state machine enters that state. After executing the entry function, the machine tries to dequeue an event from the input buffer or blocks if the buffer is empty. Upon dequeuing an event from the input queue of the machine, the attached handler is executed which might transition the machine to a different state.

This does sound it's atomic.

The example here

P/Tutorial/1_ClientServer/PSrc/Server.p

Line 26 in 8470c46

state WaitForWithdrawRequests {

both updates the database and sends a response to the client. If that is executed atomically, including event delivery, then I understand how

P/Tutorial/1_ClientServer/PSpec/BankBalanceCorrect.p

Line 36 in 8470c46

spec BankBalanceIsAlwaysCorrect observes eWithDrawReq, eWithDrawResp, eSpec_BankBalanceIsAlwaysCorrect_Init {

can be guaranteed.

However, this would actually require a transactional messaging protocol that is able to deliver a result in one distributed transaction spanning both the database update and the message delivery to the client.

Is this example simple not modeling at that detail level?

More importantly, how would I model a non-atomic database update and client response? If event handlers always run atomically, then I would need to make each of those 2 part into an own state machine?

---

So essentially, I am looking after the corresponding feature for "labels" in TLA+

Each step of the algorithm belongs to a separate label. The labels determine what happens atomically and what can be interrupted by another process. That way we can represent race conditions.

https://www.learntla.com/intro/conceptual-overview.html?highlight=label#specifications

[oberstet]

That way we can represent race conditions.

fwiw, the way that I look at this is: if I want to model realistically (eg a backend DB transaction is atomic, but not spanning a client message delivery) OR if I want to model an implementation in a "modern" programming language supporting asynchronous programming (eg. with futures/deferreds/promises or coroutines) then each "await/yield" point must be modeled as potentially branching into a new state sequence.

having a separate state machine for each asynchronous synchronization / branching point seems "wrong" .. that's my question - is it wrong? Do I fundamentally misunderstand P?

[ankushdesai]

Hi @oberstet, this is an excellent question.

A way to think about it is that each state machine is executing concurrently and the only shared state in the system (for which there can be race condition) is the inbox or message buffers. So, when any event handler in any state machine is executed, then yield or scheduling points are only inserted just before each send and receive operation so that the scheduler can interleave all sends and receives. Everything else thats executed between these sends is atomic as it only accesses local state.

Does this help?

[oberstet]

then yield or scheduling points are only inserted just before each send and receive operation so that the scheduler can interleave all sends and receives

yes, that clarifies the semantics for me, thanks! I can see the systematic/symmetry in this design. unfortunately, that's what I did suspect:( as the consequence is:

in an asynchronous program, every yield/await is a scheduling point, an independently scheduled continuation. the entry point to such a task/coroutine is a scheduling point, as is the return point. and while the latter 2 map nicely to state machine message handler entry and send message calls, the former is more general:

asynchronous continuation context can be nested, and this must be mapped to 1 state machine per asynchronous continuation context and message passing for yield/await.

eg in the "1_ClientServer" tutorial example, one would need more state machines to separate out the DB transaction and the sending of the client reply. separate from consuming a request from the inbox of the main server FSM.

practically, with such an application, stuff like this can happen:

• the app backend sent the DB transaction, but the backend crashes before receiving a DB reply
• the DB at this point now might or might not have committed
• likewise, once a DB commit success was received in the app backend, the backend might send the client reply, and before the client receives the reply, the client crashes
• ...

anyways. it'll depend I guess. however, looking from this "async app programming" perspective, I am wondering:

what I really need to exhaustively explore all possible state sequences of an async single-threaded app implementation would be: automatically use every future/promise/deferred/coroutine as a scheduling point.

those are exactly the branching points in the state sequence of such a program. wrt to the event loop / reactor (the "green threads" scheduler), not the OS of course. OS scheduling adds more branch points.

[oberstet]

I should probably add: I am mostly socialized in the context of monolithic kernels with mostly blocking system calls, and then using a green threads user program scheduler with async/await or the like. and then create a distributed app using instances of such a program.

IOW: never used microkernels, and though I have used purely message passing systems such as Erlang/OTP and purely functional (monadic IO) languages in the past, I have mostly moved to async/await style which "seems more natural".

Yeah, I know, I am not believing hard enough;) If I try very very hard, I can think about programs as just sets of assertions. Well, it seems my patience for such brain puzzles is getting lesser the older I get;) Doesn't feel natural. For me. Anyways, just my 2cts being a regular programmer ..

[oberstet]

then yield or scheduling points are only inserted just before each send and receive operation so that the scheduler can interleave all sends and receives

just rethinking this: actually, one should be able to create a devnull process that throws away every message it receives, and then just use send(devnull) to effectively yield/await at any point within an event handler?

[ankushdesai]

You can yield/await within an event handler using the receive statement in P. Which is similar to await in C#.

https://p-org.github.io/P/manual/statements/#receive

Not sure if this is what you are hinting towards in your last message?

[oberstet]

thanks for keeping this open and moving to a discussion - yeah, absolutely, isn't "an issue", but a discussion about P and semantics.

---

Not sure if this is what you are hinting towards in your last message?

yes, that was what I was hinting at: yield control, and thus inserting a branching point in the non-deterministic state sequence. however, calling receive within a state machine event handler will block until there is a message I guess. calling send would not, as message queues are unlimited size.

I don't understand the semantics fully, eg if it is possible to yield control within an event handler, and since an event handler can have local variables, this requires to save the local execution context (the continuation to be later subsumed or executed non-deterministically)?

---

In my current understanding, a model checker runs all possible sequences of execution non-deterministically, while a normal async scheduler (event loop, reactor, ..) only runs one selected (scheduled) sequence. The "scheduling/branching points" are the crucial item that structures execution into distinct/discrete steps.

In normal async programming, exactly every promise/future/deferred is a scheduling/branching point. Only 1 execution path will be taken.

In P, state machine event handler entry & exit and message send & receive are the scheduling/branching points. Every possible execution path will be taken (non-deterministic execution).

I am wondering if one could create a "non-deterministic event loop" for use in model checking.

Here is a quick check how the Python asyncio event loop deals with "1 execution path is chosen":

import sys
import asyncio

print('\n{}:'.format(sys.argv[1]))

loop = asyncio.new_event_loop()
call_at = loop.time() + 1.

n = 10
for i in range(n):
    def hello(msg):
        global n
        print(msg)
        n -= 1
        if n == 0:
            loop.stop()

    # If two callbacks are scheduled for exactly the same time, the order in which they are called is undefined.
    # https://docs.python.org/3/library/asyncio-eventloop.html#scheduling-delayed-callbacks
    loop.call_at(call_at, hello, 'hello {}'.format(i))

try:
    loop.run_forever()
finally:
    loop.close()

produces the following - notice the random but one (but interestingly fixed) order

(base) oberstet@intel-nuci7:~$ seq 3 | xargs -n 1 python test.py 

1:
hello 0
hello 2
hello 6
hello 9
hello 8
hello 5
hello 7
hello 4
hello 1
hello 3

2:
hello 0
hello 2
hello 6
hello 9
hello 8
hello 5
hello 7
hello 4
hello 1
hello 3

3:
hello 0
hello 2
hello 6
hello 9
hello 8
hello 5
hello 7
hello 4
hello 1
hello 3