search

septract / starling-tool

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

Prove the MCS queue lock using GRASShopper #133

Open septract opened 7 years ago

septract commented 7 years ago

See p154 in Herlihy & Shavit.

MattWindsor91 commented 7 years ago

@septract once the next two PRQs land, is there anything else I need to do for this?

septract commented 7 years ago

I don't think so, although other things might come up as we do the proof.

On 10 March 2017 at 11:30, Matt Windsor notifications@github.com wrote:

@septract https://github.com/septract once the next two PRQs land, is there anything else I need to do for this?

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

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