search

septract / starling-tool

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

Question-mark in views #107

Open bensimner opened 7 years ago

bensimner commented 7 years ago

Currently we allow

{| ? |} C; {| ? |}

It seems all ? does is allow hsf/muz3 to generate funcs, it'd be useful (say for dekkers) to allow us to write something like

{| ? |} <a_want = (1)>; {| AWant() * ? |}

Where we know some partial information about one thread and not about the other, for instance. I'm not sure if this would help performance of hsf as well, giving more information.

MattWindsor91 commented 7 years ago

Example is Dekker's algorithm.

This will require a bit of changing around of ViewDesugar and the view AST, to move ? from being a viewexpr-level thing to being a func-level thing.

However, it shouldn't need anything else.