State machine syntax

[MattWindsor91]

I think it'd be nice (not necessary, but nice!) to have a more concise and high-level syntax for encoding n-thread state machines in Starling.

My immediate syntax thought was eg.

fsm(min_thread, max_thread) { view name; view name; view name... };

For example, in Peterson's algorithm you might have:

fsm(0, 1) { flagDown; flagUp; waiting; holdLock };

constraint flagDown(me)      -> !flag[me] == false;
constraint flagUp(me)        -> flag[me];
constraint waiting(me)       -> flag[me];
constraint holdLock(me)      -> flag[me];

constraint holdLock(me) * holdLock(you) -> false;

automatically encoding into into (assuming we have conjunctive predicate support):

constraint flagDown(me)      -> flag[me] == false && (me >= 0 && me <= 1);
constraint flagUp(me)        -> flag[me] == true  && (me >= 0 && me <= 1);
constraint waiting(me)       -> flag[me] == true  && (me >= 0 && me <= 1);
constraint holdLock(me)      -> flag[me] == true  && (me >= 0 && me <= 1);

disjoint flagUp, flagUp;
disjoint flagUp, flagDown;
disjoint flagUp, waiting;
// and so on...

constraint holdLock(me) * holdLock(you) -> me != you && false;

My main feeling here is that doing this would A) save a lot of space in the paper for these sorts of examples, and B) have a nice story of showing that high-level patterns similar to those in iCAP etc. map into Starling's small proof core quite nicely.

[MattWindsor91]

This again becomes an interesting idea in the case of modularity: anything that uses a mutex generally needs to be a thread FSM with an attached ID.

The syntax here is probably not what we need, though. First, some FSM views can be parametric on things other than thread IDs. Second, we don't always want to bound the thread IDs.