septract / starling-tool

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

Exclusive/disjoint on view atoms? #153

Open MattWindsor91 opened 7 years ago

MattWindsor91 commented 7 years ago

I wonder if exclusive and disjoint would be more ergonomic if expressible on view atoms instead of views, e.g.

view exclusive holdLock();  // autogenerates 'constraint holdLock() * holdLock() -> false;'
view disjoint thread(int id); // autogenerates 'constraint thread(id_0) * thread(id_1) -> id_0 != id_1;'

This wouldn't work well with exclusive/disjoint constraints over different view atoms, though, unless it was a shorthand (and I'm torn as to whether Starling should have lots of syntactic sugar, or little syntactic sugar).