Cover all the examples in the Threader paper

septract commented 8 years ago

Threader is a verification tool from Andrey and co based on Horn clauses. We should cover all the examples in their CAV paper in Starling (or understand why we can't)

Threader CAV paper

Examples:

[ ] Spin2003 (standard model-checking example)
[ ] Dekker
[x] Peterson
[ ] Szymanski
[ ] Reader-writer (from Calvin model checker)
[ ] Time-varying mutex (from Calvin model checker)
[ ] NaiveBakery / Bakery
[ ] Lamport (unclear what this is?)
[ ] QRCU (the Linux RCU algorithm - verified with a fixed numbers of threads)
[ ] Mozilla-fix-vulnerab (a stock example from Mozilla CVS)
[ ] See-saw (don't know what this is)
[ ] Scull (a Linux character driver)

One observation is that Threader is limited to verifying RCU for a bounded no. of threads. We might be able to do this for unbounded threads using iterated views.

MattWindsor91 commented 7 years ago

@septract is this still in scope for CAV? Presumably not, as we have GRASShopper now…

septract commented 7 years ago

I think this is now out of scope. We need to make sure our benchmarks look okay but not cover all these examples.

On Wednesday, 11 January 2017, Matt Windsor notifications@github.com wrote:

@septract https://github.com/septract is this still in scope for CAV? Presumably not, as we have GRASShopper now…

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/88#issuecomment-271839816, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9qKy_nedfenSqPCvGknehs4JKKm5ks5rRLXwgaJpZM4K4GZR .

-- http://www-users.cs.york.ac.uk/~miked/

septract / starling-tool

Cover all the examples in the Threader paper #88