lang.v 3.68 KB
Newer Older
1
2
3
4
5
Require Import List.
Require Import RecDom.PCM.
Require Import core_lang.

(******************************************************************)
6
(** * Derived language with threadpool steps **)
7
8
(******************************************************************)

9
Module Lang (C : CORE_LANG).
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
90
91

  Export C.

  Local Open Scope lang_scope.

  (** Thread pools **)
  Definition tpool : Type := list expr.

  (** Machine configurations **)
  Definition cfg : Type := (tpool * state)%type.

  (* Threadpool stepping relation *)
  Inductive step (ρ ρ' : cfg) : Prop :=
  | step_atomic : forall e e' σ σ' K t1 t2,
      prim_step (e, σ) (e', σ') ->
      ρ  = (t1 ++ K [[ e  ]] :: t2, σ) ->
      ρ' = (t1 ++ K [[ e' ]] :: t2, σ') ->
      step ρ ρ'
  | step_fork : forall e σ K t1 t2,
      (* thread ID is 0 for the head of the list, new thread gets first free ID *)
      ρ  = (t1 ++ K [[ fork e   ]] :: t2, σ) ->
      ρ' = (t1 ++ K [[ fork_ret ]] :: t2 ++ e :: nil, σ) ->
      step ρ ρ'.

  (* Some derived facts about contexts *)
  Lemma comp_ctx_assoc K0 K1 K2 :
    (K0  K1)  K2 = K0  (K1  K2).
  Proof.
    apply (fill_inj1 _ _ fork_ret).
    now rewrite <- !fill_comp.
  Qed.

  Lemma comp_ctx_emp_l K :
    ε  K = K.
  Proof.
    apply (fill_inj1 _ _ fork_ret).
    now rewrite <- fill_comp, fill_empty.
  Qed.

  Lemma comp_ctx_emp_r K :
    K  ε = K.
  Proof.
    apply (fill_inj1 _ _ fork_ret).
    now rewrite <- fill_comp,  fill_empty.
  Qed.

  Lemma comp_ctx_inj1 K1 K2 K :
    K1  K = K2  K ->
    K1 = K2.
  Proof.
    intros HEq.
    apply fill_inj1 with (K [[ fork_ret ]]).
    now rewrite !fill_comp, HEq.
  Qed.

  Lemma comp_ctx_inj2  K K1 K2 :
    K  K1 = K  K2 ->
    K1 = K2.
  Proof.
    intros HEq.
    apply fill_inj1 with fork_ret, fill_inj2 with K.
    now rewrite !fill_comp, HEq.
  Qed.

  Lemma comp_ctx_neut_emp_r K K' :
    K = K  K' ->
    K' = ε.
  Proof.
    intros HEq.
    rewrite <- comp_ctx_emp_r in HEq at 1.
    apply comp_ctx_inj2 in HEq; congruence.
  Qed.

  Lemma comp_ctx_neut_emp_l K K' :
    K = K'  K ->
    K' = ε.
  Proof.
    intros HEq.
    rewrite <- comp_ctx_emp_l in HEq at 1.
    apply comp_ctx_inj1 in HEq; congruence.
  Qed.

92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
  (* Lemmas about expressions *)
  Lemma reducible_not_value e:
    reducible e -> ~is_value e.
  Proof.
    intros H_red H_val.
    eapply values_stuck; try eassumption.
    now erewrite fill_empty.
  Qed.

  Lemma step_same_ctx: forall K K' e e',
                         fill K e = fill K' e' ->
                         reducible e  ->
                         reducible e' ->
                         K = K'.
  Proof.
    intros K K' e e' H_fill H_red H_red'.
    edestruct (step_by_value K K' e e') as [K'' H_K''].
    - assumption.
    - assumption.
    - now apply reducible_not_value.
    - edestruct (step_by_value K' K e' e) as [K''' H_K'''].
      + now symmetry.
      + assumption.
      + now apply reducible_not_value.
      + subst K.
        rewrite comp_ctx_assoc in H_K''.
        assert (H_emp := comp_ctx_neut_emp_r _ _ H_K'').
        apply fill_noinv in H_emp.
        destruct H_emp as[H_K'''_emp H_K''_emp].
        subst K'' K'''.
        now rewrite comp_ctx_emp_r.
  Qed.

  Lemma atomic_not_stuck e:
    atomic e -> ~stuck e.
  Proof.
    intros H_atomic H_stuck.
    eapply H_stuck.
    - now erewrite fill_empty.
    - now eapply atomic_reducible.
  Qed.

134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
  Lemma fork_not_atomic K e :
    ~atomic (K [[ fork e ]]).
  Proof.
    intros HAt.
    apply atomic_not_stuck in HAt.
    apply HAt, fork_stuck.
  Qed.

  Lemma atomic_not_value e :
    atomic e -> ~is_value e.
  Proof.
    intros HAt HVal.
    apply atomic_not_stuck in HAt; apply values_stuck in HVal.
    tauto.
  Qed.

End Lang.