Commit 5887e8da authored by Simon Friis Vindum's avatar Simon Friis Vindum

Add array-based queuing lock example

parent a966fe18
......@@ -71,6 +71,10 @@ This repository contains the following case studies:
* [hocap](theories/hocap): Formalizations of the concurrent bag and concurrent
runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283)
(by Dan Frumin). See the associated [README](theories/hocap/README.md).
* [array-based_queuing-lock](/theories/array_based_queuing_lock): Proof of
safety of an implementation of the array-based queuing lock. This example is
also covered in the chapter "Case study: The Array-Based Queueing Lock" in the
Iris lecture notes.
## For Developers: How to update the Iris dependency
......
......@@ -108,3 +108,5 @@ theories/proph/lazy_coin_one_shot_typed.v
theories/proph/clairvoyant_coin_spec.v
theories/proph/clairvoyant_coin.v
theories/proph/clairvoyant_coin_typed.v
theories/array_based_queuing_lock/abql.v
\ No newline at end of file
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment