Guarantees by Construction (Mechanization)

Jules Jacobs

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
From cgraphs.locks.lambdalock Require Export langdef.

Fixpoint expr_refs e :=
  match e with
  | Val v => val_refs v
  | Var x => ∅
  | Fun x e => expr_refs e
  | App e1 e2 => expr_refs e1 ∪ expr_refs e2
  | Unit => ∅
  | Pair e1 e2 => expr_refs e1 ∪ expr_refs e2
  | LetPair e1 e2 => expr_refs e1 ∪ expr_refs e2
  | Sum i e => expr_refs e
  | MatchSum n e es => expr_refs e ∪ fin_union n (expr_refs ∘ es)
  | ForkBarrier e => expr_refs e
  | NewLock e => expr_refs e
  | ForkLock e1 e2 => expr_refs e1 ∪ expr_refs e2
  | Acquire e => expr_refs e
  | Release e1 e2 => expr_refs e1 ∪ expr_refs e2
  | Wait e => expr_refs e
  | Drop e => expr_refs e
  end
with val_refs v :=
  match v with
  | FunV x e => expr_refs e
  | UnitV => ∅
  | PairV v1 v2 => val_refs v1 ∪ val_refs v2
  | SumV i v => val_refs v
  | BarrierV i => {[ i ]}
  | LockV i => {[ i ]}
  end.

Definition obj_refs x :=
  match x with
  | Thread e => expr_refs e
  | Barrier => ∅
  | Lock refcnt o =>
      match o with
      | Some v => val_refs v
      | None => ∅
      end
  end.


Inductive expr_head_waiting : expr -> nat -> Prop :=                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d5410357 *)
  | Barrier_waiting j v :                                                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8413d160 *)
    expr_head_waiting (App (Val $ BarrierV j) (Val v)) j                         (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4b5c63ea *)
  | ForkLock_waiting j v :                                                       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a9cb5f28 *)
    expr_head_waiting (ForkLock (Val $ LockV j) (Val v)) j                       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=572908ce *)
  | Acquire_waiting j :                                                          (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ddb353d2 *)
    expr_head_waiting (Acquire (Val $ LockV j)) j                                (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3fa1fa3c *)
  | Release_waiting j v :                                                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b79e5f3 *)
    expr_head_waiting (Release (Val $ LockV j) (Val v)) j                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7d98e0bd *)
  | Wait_waiting j :                                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=857c44a5 *)
    expr_head_waiting (Wait (Val $ LockV j)) j                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=fa0e2c58 *)
  | Drop_waiting j :                                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7e46956c *)
    expr_head_waiting (Drop (Val $ LockV j)) j.                                  (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=629fe752 *)

Definition expr_waiting e j :=                                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=08f11cef *)
  ∃ k e', ctx k ∧ e = k e' ∧ expr_head_waiting e' j.                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cf20eaf3 *)

Definition waiting (ρ : cfg) (i j : nat) :=                                      (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=15f54c8b *)
  (∃ e, ρ !! i = Some (Thread e) ∧ expr_waiting e j) ∨                           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=da384fd6 *)
  (∃ y, ρ !! j = Some y ∧ i ∈ obj_refs y ∧ ∀ e, y = Thread e -> ¬ expr_waiting e i). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8fb65407 *)

Definition can_step (ρ : cfg) (i : nat) := ∃ ρ', step i ρ ρ'.
Definition inactive (ρ : cfg) (i : nat) := ρ !! i = None.

Record deadlock (ρ : cfg) (s : nat -> Prop) := {                                 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ecf26405 *)
  dl_nostep i : s i -> ¬ can_step ρ i;
  dl_waiting i j : waiting ρ i j -> s i -> s j;                                  (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=37c882b6 *)
}.

Definition deadlock_free (ρ : cfg) :=                                            (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2c70d6b6 *)
  ∀ s, deadlock ρ s -> ∀ i, s i -> inactive ρ i.                                 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9cb98e1e *)

Inductive reachable (ρ : cfg) : nat -> Prop :=                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=820718fe *)
  | Can_step_reachable i :                                                       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=768bfa19 *)
      can_step ρ i -> reachable ρ i                                              (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=767a61a7 *)
  | Waiting_reachable i j :                                                      (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=db277613 *)
      waiting ρ i j -> reachable ρ j -> reachable ρ i.                           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1b3af4d5 *)

Definition fully_reachable (ρ : cfg) :=                                          (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0652db69 *)
  ∀ i, inactive ρ i ∨ reachable ρ i.                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d4d12223 *)

Definition global_progress (ρ : cfg) :=                                          (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b4eea1d *)
  (∀ i, inactive ρ i) ∨ (∃ i, can_step ρ i).

Definition type_safety (ρ : cfg) :=                                              (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ac90f27d *)
  ∀ i, inactive ρ i ∨ can_step ρ i ∨ ∃ j, waiting ρ i j.                         (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=16dd1fe0 *)