Documentation

Mt.Reservation

class Mt.IsReservation (T : Type) extends Add , Lean.IsAssociative , Lean.IsCommutative :

Type

empty : T
empty_add : ∀ (t : T), empty + t = t

Class to represent 'reservations'

Reservations are the main method for reasoning about inter-thread behaviour.

Basic idea: Only threads with a certain reservation are allowed to do certain things. In many cases, some operation cannot be done atomically. Instead, a thread needs to do several steps. Using reservations, the thread can keep track about how many of those steps it has already accomplished. Other threads have no way to manipulate each other's reservation, only their own.

For reasoning, the reservations of all threads have to be taken into account. However, we want:

The order of the other threads should not matter
It should not matter if there are 10 other threads, or only one which achieved those reservations

As a consequence, we require an addition operator for reservations. Invariants used for reasoning may use both the shared state and the sum of all reservations, but not individual reservations. Each thread has to guarantee the invariant, but it only knows about its own reservation, i.e. it has a lower bound on the reservation, but nothing more. Therefore, it's actions are limited by the reservation it has already achieved on its own.

Example: #

There is one shared Nat variable x
Each thread performs the following three steps:
- generate a random variable n : Nat
- increase x by n + 1 atomically
- decrease x by n atomically
We want to reason that - in the end - x is never zero.

Solution: We introduce a reservation : Nat reservation which keeps track of how much we have increased x. Therefore, the have the invariant ∑reservation = x. Now, we can easily reason about the thread:
Step 1: Generating the random number has no effect on the shared variable
Step 2: We increase x by n + 1 and assign reservation :=n + 1. Since the reservations of the other threads have not changed, the invariant still holds
Step 3: Since no other thread can affect our reservation, we still know that reservation = n + 1. Because of our invariant, we also know x = ∑reservation ≥ reservation = n + 1. Therefore, we can safely decrease both x and reservation by n and we still have x > 0

Instances

structure Mt.Spec :

Type 1

State : Type
Reservation : Type
is_reservation : Mt.IsReservation Reservation
validate : Reservation → State → Prop

Specification for a multithreading system

This specification specifies the context for threads but not the threads itself. Threads encode a specification in their type. Only threads with the same specification can be executed in parallel

Instances For

instance Mt.instIsReservationNat :

Mt.IsReservation Nat

Equations

Mt.instIsReservationNat = Mt.IsReservation.mk 0 Nat.zero_add

def Mt.LowerBound :

Type

Equations

Mt.LowerBound = Nat

instance Mt.instAddLowerBound :

Add Mt.LowerBound

Equations

Mt.instAddLowerBound = { add := Nat.max }

instance Mt.LowerBound.instance :

Mt.IsReservation Mt.LowerBound

Equations

Mt.LowerBound.instance = Mt.IsReservation.mk 0 Mt.Utils.Nat.zero_max

structure Mt.UnitReservation :

Type

Instances For

instance Mt.instIsReservationUnitReservation :

Mt.IsReservation Mt.UnitReservation

Equations

Mt.instIsReservationUnitReservation = Mt.IsReservation.mk { } Mt.instIsReservationUnitReservation.proof_3

inductive Mt.Lock (T : Type) :

Type

Unlocked: {T : Type} → Mt.Lock T
Locked: {T : Type} → T → Mt.Lock T
Invalid: {T : Type} → Mt.Lock T

Instances For

def Mt.Lock.is_locked {T : Type} :

Mt.Lock T → Bool

Equations

Mt.Lock.is_locked _fun_discr = match _fun_discr with | Mt.Lock.Locked a => true | x => false

def Mt.Lock.is_locked_and_valid {T : Type} (valid : T → Prop) :

Mt.Lock T → Prop

Equations

Mt.Lock.is_locked_and_valid valid _fun_discr = match _fun_discr with | Mt.Lock.Locked s => valid s | x => False

def Mt.Lock.is_unlocked {T : Type} :

Mt.Lock T → Bool

Equations

Mt.Lock.is_unlocked _fun_discr = match _fun_discr with | Mt.Lock.Unlocked => true | x => false

def Mt.Lock.add {T : Type} :

Mt.Lock T → Mt.Lock T → Mt.Lock T

Equations

Mt.Lock.add _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Mt.Lock.Unlocked, a => a | a, Mt.Lock.Unlocked => a | x, x_1 => Mt.Lock.Invalid

theorem Mt.Lock.eq_of_is_unlocked {T : Type} {r : Mt.Lock T} :

Mt.Lock.is_unlocked r = true → r = Mt.Lock.Unlocked

instance Mt.instAddLock {T : Type} :

Add (Mt.Lock T)

Equations

Mt.instAddLock = { add := Mt.Lock.add }

theorem Mt.Lock.unlocked_add {T : Type} (a : Mt.Lock T) :

Mt.Lock.Unlocked + a = a

theorem Mt.Lock.add_unlocked {T : Type} (a : Mt.Lock T) :

a + Mt.Lock.Unlocked = a

theorem Mt.Lock.invalid_add {T : Type} (a : Mt.Lock T) :

Mt.Lock.Invalid + a = Mt.Lock.Invalid

theorem Mt.Lock.add_comm {T : Type} (a : Mt.Lock T) (b : Mt.Lock T) :

a + b = b + a

theorem Mt.Lock.add_assoc {T : Type} (a : Mt.Lock T) (b : Mt.Lock T) (c : Mt.Lock T) :

a + b + c = a + (b + c)

instance Mt.instIsReservationLock {T : Type} :

Mt.IsReservation (Mt.Lock T)

Equations

Mt.instIsReservationLock = Mt.IsReservation.mk Mt.Lock.Unlocked (_ : ∀ (a : Mt.Lock T), Mt.Lock.Unlocked + a = a)