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
From cgraphs.locks.lambdalock Require Import invariant.


Lemma fully_reachable_iff_deadlock_free ρ :                                      (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ef7b15bb *)
  fully_reachable ρ <-> deadlock_free ρ.
Proof.
  split.
  - intros Hfr s [] i si.
    destruct (Hfr i); eauto.
    exfalso. induction H; naive_solver.
  - intros Hdf i. classical_left.
    eapply (Hdf (λ i, ¬ reachable ρ i));
    first constructor; eauto using reachable.
Qed.

Lemma fully_reachable_type_safety ρ :                                            (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=95d5a036 *)
  fully_reachable ρ -> type_safety ρ.
Proof.
  intros Hfr i. destruct (Hfr i) as [|[]]; eauto.
Qed.

Lemma fully_reachable_global_progress ρ :                                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0fdaf312 *)
  fully_reachable ρ -> global_progress ρ.
Proof.
  intros Hfr.
  destruct (classic (∃ i, ¬ inactive ρ i)).
  - destruct H as [i Hi]. destruct (Hfr i); first naive_solver.
    clear Hi. right. induction H; eauto.
  - left. intros i. apply NNPP. eauto.
Qed.

Lemma typed_full_reachability e ρ :                                              (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5d66e44f *)
  typed ∅ e UnitT -> steps {[ 0 := Thread e ]} ρ -> fully_reachable ρ.
Proof.
  intros Ht Hsteps.
  assert (ginv {[ 0 := Thread e ]}) as Hinv.
  { eapply initialization. done. }
  induction Hsteps.
  - eapply full_reachability. done.
  - eapply IHHsteps. destruct H. eapply preservation; eauto.
Qed.

Lemma typed_global_progress e ρ :                                                (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=99029a1e *)
  typed ∅ e UnitT -> steps {[ 0 := Thread e ]} ρ -> global_progress ρ.
Proof.
  intros. eapply fully_reachable_global_progress, typed_full_reachability; done.
Qed.