search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

State machine syntax #122

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

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 commented 7 years ago

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.