exercises.ticket_lock

From iris.algebra Require Import auth excl gset numbers.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Import lang proofmode notation.

(* ################################ *)

Case Study: Ticket Lock

(* ================================================================= *)

Implementation

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.

Definition mk_lock : val :=
  λ: <>, (ref #0, ref #0).

Definition wait : val :=
  rec: "wait" "n" "l" :=
  let: "o" := !(Fst "l") in
  if: "o" = "n" then #() else "wait" "n" "l".

Definition acquire : val :=
  rec: "acquire" "l" :=
  let: "n" := !(Snd "l") in
  if: CAS (Snd "l") "n" ("n" + #1) then
    wait "n" "l"
  else
    "acquire" "l".

Definition release : val :=
  λ: "l", Fst "l" <- ! (Fst "l") + #1.

(* ================================================================= *)

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
(* := insert your definition here *). Admitted.

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 Σ
(* := insert your definition here *). Admitted.

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.
Proof.
(* exercise *)
Admitted.

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 Σ
  (* := insert your definition here *). Admitted.

Definition lock_inv (γ : gname) (lo ln : loc) (P : iProp Σ) : iProp Σ
  (* := insert your definition here *). Admitted.

Definition is_lock (γ : gname) (l : val) (P : iProp Σ) : iProp Σ :=
  ∃ lo ln : loc, ⌜l = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln P).

(* ================================================================= *)

Specifications

Lemma mk_lock_spec P :
  {{{ P }}} mk_lock #() {{{ γ l, RET l; is_lock γ l P }}}.
Proof.
  (* exercise *)
Admitted.

Lemma wait_spec γ l P x :
  {{{ is_lock γ l P ∗ issued γ x }}}
    wait #x l
  {{{ RET #(); locked γ ∗ P }}}.
Proof.
  (* exercise *)
Admitted.

Lemma acquire_spec γ l P :
  {{{ is_lock γ l P }}} acquire l {{{ RET #(); locked γ ∗ P }}}.
Proof.
  (* exercise *)
Admitted.

Lemma release_spec γ l P :
  {{{ is_lock γ l P ∗ locked γ ∗ P }}} release l {{{ RET #(); True }}}.
Proof.
  (* exercise *)
Admitted.

End proofs.