Updated todo and readme. Cleaned up ticket_lock_advanced. Added contributors.

Author: MatteP1

README.md

@@ -1,7 +1,7 @@
 # Iris Tutorial
 The Iris Tutorial is an introduction to the [Iris separation logic framework](https://iris-project.org/) and how to work with its [Coq formalization](https://gitlab.mpi-sws.org/iris/iris/).
 
-The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Coq proof assistant is assumed. Advanced Coq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning.
+The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Coq proof assistant is assumed. Advanced Coq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning. We demonstrate more advanced tactics in chapter [ticket_lock_advanced](/theories/ticket_lock_advanced.v).
 
 The tutorial comes in two versions:
 
@@ -57,6 +57,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-
 - [counter](/exercises/counter.v) - The authoritative camera
 - [spin_lock](/exercises/spin_lock.v) - Specification of a spin lock
 - [ticket_lock](/exercises/ticket_lock.v) - Specification of a ticket lock
+- [ticket_lock_advanced](/theories/ticket_lock_advanced.v) - Advanced Coq tactics
 - [adequacy](/exercises/adequacy.v) - Adequacy
 - [merge_sort](/exercises/merge_sort.v) - Merge sort
 - [custom_ra](/exercises/custom_ra.v) - Defining resource algebras from scratch
@@ -196,4 +197,19 @@ If you have specific requests or questions about the tutorial, please contact:
 
 **Amin Timany**\
 Aarhus University\
-<timany@cs.au.dk>
+<timany@cs.au.dk>
+
+### Contributors
+Below is a list of people who have contributed to the tutorial, sorted by last name. If you have contributed to the project, please add yourself to the list.
+
+**Lars Birkedal**\
+Aarhus University\
+<birkedal@cs.au.dk>
+
+**Mathias Pedersen**\
+Aarhus University\
+<mp@cs.au.dk>
+
+**Amin Timany**\
+Aarhus University\
+<timany@cs.au.dk>

TODO.md

@@ -1,5 +1,11 @@
+# Fixes
+- Clean up proofs in some chapters
+  - Reduce use of SSreflect
+  - Simplify proofs
+
 # Possible future topics
-- Have a file showcasing advanced Coq tactics.
+- Chapter on prophecies
+- Chapter on HOCAP-style specifications
 - Chapters "Linked List", "Arrays", and "Merge Sort" all use list functionality from std++ (e.g. fmap and lookup). These should be introduced beforehand, for example in an appendix, with the chapters referring to the appendix.
 - Consider introducing commands "About", "Locate", "Print", etc. in an introductory chapter.
 - Add example with "Landin's knot" (recursion through the store) to showcase use of dicardable fractions or invariants for sequential programs

theories/ticket_lock_advanced.v

@@ -3,34 +3,17 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import lang proofmode notation.
 
 (* ################################################################# *)
-(** * Case Study: Ticket Lock *)
-
-(* ================================================================= *)
-(** ** Implementation *)
+(** * Case Study: Ticket Lock Advanced *)
 
 (**
-  Let us look at another implementation of a lock, namely a ticket lock.
-  Instead of having every thread fight to acquire the lock, the ticket
-  lock makes them wait in line. It functions similarly to a ticketing
-  system that one often finds in bakeries and pharmacies. Upon entering
-  the shop, you pick a ticket with some number and wait until the number
-  on the screen has reached your number. Once this happens, it becomes
-  your turn to speak to the shop assistant. In our scenario, talking to
-  the shop assistant corresponds to accessing the protected resources.
-
-  To implement this, we will maintain two counters: [o] and [n]. The
-  first counter, [o], represents the number on the screen – the customer
-  currently being served. The second counter, [n], represents the next
-  number to be dispensed by the ticketing machine.
-
-  To acquire the lock, a thread must increment the second counter, [n],
-  and keep its previous value as a ticket for a position in the queue.
-  Once the ticket has been obtained, the thread must wait until the
-  first counter, [o], reaches its ticket value. Once this happens, the
-  thread gets access to the protected resources. The thread can then
-  release the lock by incrementing the first counter.
+  The implementation, resource algebra, and representation predicates
+  are identical to the original Ticket Lock chapter. Only the proofs
+  differ.
 *)
 
+(* ================================================================= *)
+(** ** Implementation *)
+
 Definition mk_lock : val :=
   λ: <>, (ref #0, ref #0).
 
@@ -53,98 +36,35 @@ Definition release : val :=
 (* ================================================================= *)
 (** ** Representation Predicates *)
 
-(**
-  As a ticket lock is a lock, we expect it to satisfy the same
-  specification as the spin-lock. This time, you have to come up with
-  the necessary resource algebra and lock invariant by yourself. It
-  might be instructive to first look through all required predicates and
-  specifications to figure out exactly what needs to be proven.
-*)
-
-Definition RA : cmra
-(* BEGIN SOLUTION *)
-  (**
-    We will use a finite set of numbers to represent the tickets that
-    have been issued – the second counter. This becomes a camera by
-    using the disjoint union as an operation.
-
-    For the first counter, we will use the exclusive camera over the
-    natural numbers – this means that there can be only one
-    access-granting ticket owned at a time.
-
-    By wrapping them both in an authoritative camera, we can use the
-    authoritative fragment to bind the values of our counters to the
-    ghost state.
-  *)
-  := authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)).
-(* END SOLUTION BEGIN TEMPLATE
-  (* := insert your definition here *). Admitted.
-END TEMPLATE *)
+Definition RA : cmra :=
+  authR (prodUR (optionUR (exclR natO)) (gset_disjR nat)).
 
 Section proofs.
 Context `{!heapGS Σ, !inG Σ RA}.
 Let N := nroot .@ "ticket_lock".
 
-(**
-  This time around, we know that the thread is locked by a thread with a
-  specific ticket. As such, we first define a predicate [locked_by]
-  which states that the lock is locked by ticket [o].
-*)
-Definition locked_by (γ : gname) (o : nat) : iProp Σ
-(* BEGIN SOLUTION *)
-  (**
-    We know that the lock is locked by ticket [o] when we have ownership
-    of the exclusive counter being [o].
-  *)
-  := own γ (◯ (Excl' o, GSet ∅)).
-(* END SOLUTION BEGIN TEMPLATE
-  (* := insert your definition here *). Admitted.
-END TEMPLATE *)
+Definition locked_by (γ : gname) (o : nat) : iProp Σ :=
+  own γ (◯ (Excl' o, GSet ∅)).
 
-(** The lock is locked when it has been locked by some ticket. *)
 Definition locked (γ : gname) : iProp Σ :=
   ∃ o, locked_by γ o.
 
 Lemma locked_excl γ : locked γ -∗ locked γ -∗ False.
-(* SOLUTION *) Proof.
+Proof.
   iIntros "[%o1 H1] [%o2 H2]".
   iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_valid_1; done.
 Qed.
 
-(**
-  We will also have a predicate signifying that ticket [x] has been
-  _issued_. A thread will need to have been issued ticket [x] in order
-  to wait for the first counter to become [x].
-*)
-Definition issued (γ : gname) (x : nat) : iProp Σ
-(* BEGIN SOLUTION *)
-  (** A ticket is simply the singleton set over its index. *)
-  := own γ (◯ (ε : option (excl nat), GSet {[x]})).
-(* END SOLUTION BEGIN TEMPLATE
-  (* := insert your definition here *). Admitted.
-END TEMPLATE *)
-
-Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ
-(* BEGIN SOLUTION *)
-  (**
-    Our invariant will first link the authoritative fragment to the
-    counters. For the second counter, this means that all tickets prior
-    to the counter's current value must have been issued.
+Definition issued (γ : gname) (x : nat) : iProp Σ :=
+  own γ (◯ (ε : option (excl nat), GSet {[x]})).
 
-    Secondly, the lock contains either ownership of the value of the
-    first counter as well as the protected resources (the queue is
-    unlocked), or the current access-granting ticket (the queue is
-    locked).
-  *)
-  := ∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗
+Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ :=
+  ∃ o n : nat, lo ↦ #o ∗ ln ↦ #n ∗
   own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
   (
     (locked_by γ o ∗ P) ∨
     issued γ o
   ).
-(* END SOLUTION BEGIN TEMPLATE
-  (* := insert your definition here *). Admitted.
-END TEMPLATE *)
 
 Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ :=
   ∃ lo ln : loc, ⌜l = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln P).
@@ -154,7 +74,7 @@ Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ :=
 
 Lemma mk_lock_spec P :
   {{{ P }}} mk_lock #() {{{ γ l, RET l; is_lock γ l P }}}.
-(* SOLUTION *) Proof.
+Proof.
   iIntros "%Φ HP HΦ".
   wp_lam.
   wp_alloc lo; wp_alloc ln.
@@ -170,7 +90,7 @@ Lemma wait_spec γ l P x :
   {{{ is_lock γ l P ∗ issued γ x }}}
     wait #x l
   {{{ RET #(); locked γ ∗ P }}}.
-(* SOLUTION *) Proof.
+Proof.
   iIntros "%Φ [(%lo & %ln & -> & #I) Hx] HΦ".
   iLöb as "IH".
   wp_rec.
@@ -199,7 +119,7 @@ Qed.
 
 Lemma acquire_spec γ l P :
   {{{ is_lock γ l P }}} acquire l {{{ RET #(); locked γ ∗ P }}}.
-(* SOLUTION *) Proof.
+Proof.
   iIntros "%Φ (%lo & %ln & -> & #I) HΦ".
   iLöb as "IH".
   wp_rec.
@@ -236,7 +156,7 @@ Qed.
 
 Lemma release_spec γ l P :
   {{{ is_lock γ l P ∗ locked γ ∗ P }}} release l {{{ RET #(); True }}}.
-(* SOLUTION *) Proof.
+Proof.
   iIntros "%Φ ((%lo & %ln & -> & #I) & [%o Hexcl] & HP) HΦ".
   wp_lam.
   wp_pures.