Library models.LinCCAL

Require Import FMapPositive.
Require Import Relation_Operators Operators_Properties.
Require Import Program.
Require Import Classical.

Require Import coqrel.LogicalRelations.
Require Import interfaces.Category.
Require Import models.EffectSignatures.

Linearization-based Concurrent Certified Abstraction Layers


Module LinCCAL <: Category.

  Module TMap := PositiveMap.
  Notation tid := TMap.key.
  Notation tmap := TMap.t.

Concurrent object specifications

For simplicity, we use linearized atomic specifications and specify correctness directly in terms of that model. In their linearized form, the specifications are deterministic, however we allow both undefined and unimplementable behaviors. Undefined behaviors (spec_bot) release the implementation of any obligation, and are usually a consequence of illegal actions by the client (for example, a thread acquiring a lock twice). Conversely, unimplementable behaviors (spec_top) are simply impossible for an implementation to obey; this is usually meant to force a different linearization order. For example, in the atomic specification, acquiring a lock which is already held by a different thread will yield an unimplementable spec. However, a lock implementation can still obey the specification by delaying the linearization of acquire until the lock is released by the thread currently holding it.

  CoInductive spec_after {E : Sig.t} {m : Sig.op E} :=
    (*
    | spec_bot
     *)
    | spec_top
    | spec_cons (n : Sig.ar m) (k : tid → ∀ m, @spec_after E m).

  Arguments spec_after : clear implicits.

  Notation spec E := (tid → ∀ m, spec_after E m).

To formalize this interpretation, we can describe the possible outcomes of performing the next invocation in a specification, namely the admissible return values and specification next states.

  (*
  Variant spec_query {E m} (n: Sig.ar m) (k: spec E) : spec_after E m -> Prop :=
    | spec_query_bot : spec_query n k spec_bot
    | spec_query_cons : spec_query n k (spec_cons n k).

  Definition spec_next {E} (Σ : spec E) t m n k : Prop :=
    spec_query n k (Σ t m).
   *)

Implementation states

We use regular maps Reg.m to model implementations of a given overlay specification in terms of a given underlay specification. A regular map associates with each overlay operation a term of the underlay signature, interpreted as a strategy tree or a computation in the free monad, in the style of algebraic effect frameworks.
To express correctness, we use the following execution model. When a method ts_op is invoked in a particular thread, we use the implementation to initialize a computation ts_prog for that thread. Whenever the thread is scheduled, we use the (linearized, atomic) underlay specification to perform the next underlay call in the computation. Eventually, the computation will produce a result and return from the overlay call.
It remains to compare this behavior to the one prescribed by the overlay specification. To prove that the implementation's behavior linearizes to the atomic overlay specification, we must show there is a way to pick a particular point in time, as a method is being executed, when its atomic call and return will be recoded as occuring from the point of view of the overlay client. We match the call against the overlay specification at that time and keep track of the result ts_res that we have committed to. As the method's execution proceeds and eventually terminates, we will have to show that the actual outcome matches the recorded result.
Concretely, our state will consist of a finite map which will associate to each running thread a linearization state of the following type.

  Record threadstate {E F : Sig.t} :=
    mkts {
      ts_op : Sig.op F;
      ts_prog : Sig.term E (Sig.ar ts_op);
      ts_res : option (Sig.ar ts_op);
    }.

  Arguments threadstate : clear implicits.
  Arguments mkts {E F}.

Then the global state consists of a thread state for every running thread, an overlay spec and an underlay spec.

  Record state {E F} :=
    mkst {
      st_spec : spec F;
      st_impl :> tmap (threadstate E F);
      st_base : spec E;
    }.

  Arguments state : clear implicits.
  Arguments mkst {E F}.

Environment steps

At any time, the environment may invoke a method on a ready thread, or schedule a running thread to execute. A linearization proof must be ready to deal with the corresponding effects on the state, enumerated below.

  Variant estep {E F} (M : Reg.Op.m E F) : relation (state E F) :=
    | einvoke t q Δ s s' Σ :
        TMap.find t s = None →
        TMap.add t (mkts q (M q) None) s = s' →
        estep M (mkst Δ s Σ) (mkst Δ s' Σ)
    | eaction t q m n k R Δ s Σ s' Σ' :
        TMap.find t s = Some (mkts q (Sig.cons m k) R) →
        Σ t m = spec_cons n Σ' →
        TMap.add t (mkts q (k n) R) s = s' →
        estep M (mkst Δ s Σ) (mkst Δ s' Σ')
    | ereturn t q r Δ s s' Σ :
        TMap.find t s = Some (mkts q (Sig.var r) (Some r)) →
        TMap.remove t s = s' →
        estep M (mkst Δ s Σ) (mkst Δ s' Σ).

Commit steps

Our job is then to insert commit steps in such a way that by the time ereturn is in play, the invocation has been committed with the correct outcome.

  Variant lstep {E F} : relation (state E F) :=
    | lcommit t q r T Δ Δ' s s' Σ :
        TMap.find t s = Some (mkts q T None) →
        Δ t q = spec_cons r Δ' →
        TMap.add t (mkts q T (Some r)) s = s' →
        lstep (mkst Δ s Σ) (mkst Δ' s' Σ).

Correctness

Based on the constructions above, our ultimate goal is to show that no matter what methods are called and how the threads are scheduled, there is a way to perform commits such that the following invariant is always preserved. That is, every thread will eventually produce the result that was matched against the overlay specification.

  Definition threadstate_valid {E F} (e : option (threadstate E F)) :=
    ∀ q r R, e = Some (mkts q (Sig.var r) R) → R = Some r.

Note that if spec_top appears in the underlay specification Σ, there will be no corresponding eaction step to take. As a result the associated thread will not be scheduled and there are no correctness requirements against it at that time. Conversely, if spec_top appears in the overlay specification Δ, there will be no way to commit a result at that point in time.

Rechability predicate

To formulate this criterion, we will use the following helpful definitions and properties.

  Notation star := (clos_refl_trans _).

  Definition reachable {A} (R : relation A) (P : A → Prop) (x : A) :=
    ∃ y, star R x y ∧ P y.

  Lemma reachable_base {A} (R : relation A) (P : A → Prop) (x : A) :
    P x → reachable R P x.

  Lemma reachable_step {A} (R : relation A) P x y :
    reachable R P y →
    R x y →
    reachable R P x.

  Lemma reachable_steps {A} (R : relation A) (P : A → Prop) (x y : A) :
    reachable R P y →
    star R x y →
    reachable R P x.

  Lemma lsteps_ind {E F} (P : spec F → _ → spec E → Prop) (Q : state E F → Prop) :
    (∀ Δ v Σ,
        Q (mkst Δ v Σ) →
        P Δ v Σ) →
    (∀ t q r T Δ Δ' s Σ,
        TMap.find t s = Some (mkts q T None) →
        Δ t q = spec_cons r Δ' →
        P Δ' (TMap.add t (mkts q T (Some r)) s) Σ →
        P Δ s Σ) →
    (∀ Δ v Σ,
        reachable lstep Q (mkst Δ v Σ) →
        P Δ v Σ).

Coinductive property

The overall correctness property can be given as follows.

  CoInductive correct {E F} (M : Reg.Op.m E F) (s : state E F) : Prop :=
    {
      correct_valid :
        ∀ i, threadstate_valid (TMap.find i s);
      correct_next :
        ∀ s', estep M s s' → reachable lstep (correct M) s';
    }.

  Definition cal {E F} Σ (M : Reg.Op.m E F) Δ :=
    correct M (mkst Δ (TMap.empty _) Σ).

Proof method

To establish correctness, it suffices to show that there is a correctness invariant with the following properties.

  Record correctness_invariant {E F} (M : Reg.Op.m E F) (P : state E F → Prop) : Prop :=
    {
      ci_valid s :
        P s → ∀ i, threadstate_valid (TMap.find i s);
      ci_next s :
        P s → ∀ s', estep M s s' → reachable lstep P s';
    }.

  Lemma correct_ci {E F} (M : Reg.Op.m E F) :
    correctness_invariant M (correct M).

  Lemma correctness_invariant_sound {E F} (M : Reg.Op.m E F) P :
    correctness_invariant M P →
    ∀ s, P s → correct M s.

Identity


  Variant id_linstate {E} : threadstate E E → Prop :=
    | id_invoked q :
      id_linstate (mkts q (Sig.cons q Sig.var) None)
    | id_returned q r :
      id_linstate (mkts q (Sig.var r) (Some r)).

  Variant id_state {E} : state E E → Prop :=
    id_state_intro Σ (u : tmap (threadstate E E)) :
      (∀ t s, TMap.find t u = Some s → id_linstate s) →
      id_state (mkst Σ u Σ).

  Lemma id_state_ci E :
    correctness_invariant (Reg.id E) id_state.

  Theorem id_cal {E} (Σ : spec E) :
    cal Σ (Reg.id E) Σ.

Composition


  Notation "t >>= f" := (Sig.subst f t) (left associativity, at level 40).
  Notation "x <- t ; f" := (t >>= fun x ⇒ f) (right associativity, at level 60).

  Section COMPOSE.
    Context {E F G} (M : Reg.Op.m F G) (N : Reg.Op.m E F).

Per-thread invariant

When M invokes a method m of N with continuation k, we distinguish between two phases:
  • before N commits a result, the action is still pending in M
  • afterwards, M progresses and is now waiting on the next action (or return), which will be carried out after N actually returns.
In order to express this, we introduce the following auxiliary computation, which computes the current program of M based on the commit state S of the N component.

    Definition pending_program (q: Sig.op G) m k S : Sig.term F (Sig.ar q) :=
      match S with
        | None ⇒ Sig.cons m k
        | Some n ⇒ k n
      end.

The predicate we use to formulate the composition invariant will also cover intermediate states where internal execution is ongoing. This is the case when a thread has a Sig.cons program in M while N is waiting for the next query, or when N has a Sig.var program. We will use the following constructions to manage this.

    Variant comp_phase :=
      | comp_ready
      | comp_running (i : tid) (q : Sig.op G) (T : Sig.term F (Sig.ar q)).

    Variant run_check_l i q : Sig.term F (Sig.ar q) → comp_phase → Prop :=
      | run_check_l_cons m mk :
        run_check_l i q (Sig.cons m mk) (comp_running i q (Sig.cons m mk))
      | run_check_l_var w r :
        run_check_l i q (Sig.var r) w.

    Variant run_check_r i q m mk : Sig.term E (Sig.ar m) → _ → Prop :=
      | run_check_r_cons u uk w :
        run_check_r i q m mk (Sig.cons u uk) w
      | run_check_r_var n :
        run_check_r i q m mk (Sig.var n) (comp_running i q (Sig.cons m mk)).

The predicate comp_threadstate i w s12 s1 s2 relates the composite state s12 for thread i with the component states s1 and s2. The parameter w optionally allows a thread to be running, so that unprocessed internal interactions could still be present if that thread matches i.

    Variant comp_threadstate i (w : comp_phase) : _ → _ → _ → Prop :=
      (* The thread is currently waiting for the next query. *)
      | cts_ready :
        comp_threadstate i w
          None
          None
          None
      (* Query q is being executed by M with the remaning program T.
         N is not running. *)
      | cts_left q T R :
        run_check_l i q T w →
        comp_threadstate i w
          (Some (mkts q (Reg.transform N T) R))
          (Some (mkts q T R))
          None
      (* Query q is begin executed by M, which has invoked N
         with the query m. Once the remaining program U in N
         returns a result n, the execution of M is resumed
         according to mk n. *)
      | cts_right q m U Q mk R :
        run_check_r i q m mk U w →
        comp_threadstate i w
          (Some (mkts q (n <- U; Reg.transform N (mk n)) R))
          (Some (mkts q (pending_program q m mk Q) R))
          (Some (mkts m U Q)).

    Lemma comp_threadstate_valid i e12 e1 e2 :
      comp_threadstate i comp_ready e12 e1 e2 →
      threadstate_valid e1 →
      threadstate_valid e2 →
      threadstate_valid e12.

    Lemma comp_threadstate_o i j q T w s12 s1 s2 :
      comp_threadstate i (comp_running j q T) s12 s1 s2 →
      i ≠ j →
      comp_threadstate i w s12 s1 s2.

Global state invariant


    Definition comp_tmap w (s12 s1 s2 : tmap (threadstate _ _)) : Prop :=
      ∀ i,
        comp_threadstate i w (TMap.find i s12) (TMap.find i s1) (TMap.find i s2).

    Lemma comp_tmap_convert t q T w s12 s1 s2 :
      comp_tmap (comp_running t q T) s12 s1 s2 →
      comp_threadstate t w (TMap.find t s12) (TMap.find t s1) (TMap.find t s2) →
      comp_tmap w s12 s1 s2.

The invariant is preserved by environment steps.

    Lemma comp_tmap_invoke_l s12 s1 s2 t q :
      TMap.find t s1 = None →
      comp_tmap comp_ready s12 s1 s2 →
      comp_tmap (comp_running t q (M q))
        (TMap.add t (mkts q (Reg.Op.compose M N q) None) s12)
        (TMap.add t (mkts q (M q) None) s1)
        s2.

    Lemma comp_tmap_action_l w t q m n mk U R s12 s1 s2 :
      TMap.find t s1 = Some (mkts q (Sig.cons m mk) R) →
      TMap.find t s2 = Some (mkts m U None) →
      comp_tmap w s12 s1 s2 →
      comp_tmap w s12 (TMap.add t (mkts q (mk n) R) s1)
                      (TMap.add t (mkts m U (Some n)) s2).

    Lemma comp_tmap_return_l w t q r s12 s1 s2 :
      TMap.find t s1 = Some (mkts q (Sig.var r) (Some r)) →
      TMap.find t s2 = None →
      comp_tmap w s12 s1 s2 →
      comp_tmap w (TMap.remove t s12) (TMap.remove t s1) s2.

    Lemma comp_tmap_invoke_r s12 s1 s2 t q m mk R w :
      TMap.find t s1 = Some (mkts q (Sig.cons m mk) R) →
      TMap.find t s2 = None →
      comp_tmap w s12 s1 s2 →
      comp_tmap w s12 s1 (TMap.add t (mkts m (N m) None) s2).

    Lemma comp_tmap_action_r s12 s1 s2 t q m mk u uk v R S :
      TMap.find t s1 = Some (mkts q (pending_program q m mk S) R) →
      TMap.find t s2 = Some (mkts m (Sig.cons u uk) S) →
      comp_tmap comp_ready s12 s1 s2 →
      comp_tmap (comp_running t q (Sig.cons m mk))
                (TMap.add t (mkts q (n <- uk v; Reg.transform N (mk n)) R) s12)
                s1
                (TMap.add t (mkts m (uk v) S) s2).

    Lemma comp_tmap_return_r s12 s1 s2 t q m mk n :
      TMap.find t s2 = Some (mkts m (Sig.var n) (Some n)) →
      comp_tmap (comp_running t q (Sig.cons m mk)) s12 s1 s2 →
      comp_tmap (comp_running t q (mk n)) s12 s1 (TMap.remove t s2).

The commit steps triggered by the components likewise perserve the invariant, once equivalent commit steps have been applied to the composite layer as needed.

    Lemma comp_tmap_commit_l Δ s1 Γ s2 Σ s12 p :
      reachable lstep (correct M) (mkst Δ s1 Γ) →
      comp_tmap p s12 s1 s2 →
      ∃ Δ' s12' s1',
        star lstep (mkst Δ s12 Σ) (mkst Δ' s12' Σ) ∧
        correct M (mkst Δ' s1' Γ) ∧
        comp_tmap p s12' s1' s2.

    Lemma comp_tmap_commit_r w Δ s1 Γ s2 Σ s12 :
      reachable lstep (correct N) (mkst Γ s2 Σ) →
      correct M (mkst Δ s1 Γ) →
      comp_tmap w s12 s1 s2 →
      ∃ Δ' Γ' s12' s1' s2',
        star lstep (mkst Δ s12 Σ) (mkst Δ' s12' Σ) ∧
        correct M (mkst Δ' s1' Γ') ∧
        correct N (mkst Γ' s2' Σ) ∧
        comp_tmap w s12' s1' s2' ∧
        ∀ i, TMap.find i s2 ≠ None → TMap.find i s2' ≠ None.

Overall invariant

The overall composition invariant is as follows. Essentially, there should be an intemediate specification and component states such that each thread satisfies comp_threadstate, and such that the component are correct with respect to the relevant specifications.

    Variant comp_state w : state E G → Prop :=
      comp_state_intro Σ Γ Δ s12 s1 s2 :
        comp_tmap w s12 s1 s2 →
        correct M (mkst Δ s1 Γ) →
        correct N (mkst Γ s2 Σ) →
        comp_state w (mkst Δ s12 Σ).

    Lemma comp_run_r t q m mk s12 Δ s1 Γ s2 Σ :
      comp_tmap (comp_running t q (Sig.cons m mk)) s12 s1 s2 →
      correct M (mkst Δ s1 Γ) →
      correct N (mkst Γ s2 Σ) →
      TMap.find t s2 ≠ None →
      (∀ n s,
          comp_state (comp_running t q (mk n)) s →
          reachable lstep (comp_state comp_ready) s) →
      reachable lstep (comp_state comp_ready) (mkst Δ s12 Σ).

    Lemma comp_run t q T s :
      comp_state (comp_running t q T) s →
      reachable lstep (comp_state comp_ready) s.

    Lemma comp_ci :
      correctness_invariant (Reg.Op.compose M N) (comp_state comp_ready).

    Theorem comp_cal Σ Γ Δ :
      cal Γ M Δ →
      cal Σ N Γ →
      cal Σ (Reg.Op.compose M N) Δ.
  End COMPOSE.

Certified abstraction layers form a category


  Record layer_interface :=
    {
      li_sig : Sig.t;
      li_spec : spec li_sig;
    }.

  Record layer_implementation {L L' : layer_interface} :=
    {
      li_impl : Reg.Op.m (li_sig L) (li_sig L');
      li_correct : cal (li_spec L) li_impl (li_spec L');
    }.

  Arguments layer_implementation : clear implicits.

  Definition t : Type := layer_interface.
  Definition m : t → t → Type := layer_implementation.

  Program Definition id L : m L L :=
    {| li_impl := Reg.id (li_sig L) |}.

  Program Definition compose {L1 L2 L3} (M : m L2 L3) (N : m L1 L2) :=
    {| li_impl := Reg.Op.compose (li_impl M) (li_impl N) |}.

  Lemma meq {L1 L2} (M N : m L1 L2) :
    li_impl M = li_impl N → M = N.

  Lemma compose_id_left {L1 L2} (M : m L1 L2) :
    compose (id L2) M = M.

  Lemma compose_id_right {L1 L2} (M : m L1 L2) :
    compose M (id L1) = M.

  Lemma compose_assoc {L1 L2 L3 L4} (M12: m L1 L2) (M23: m L2 L3) (M34: m L3 L4):
    compose (compose M34 M23) M12 = compose M34 (compose M23 M12).

  Include CategoryTheory.
End LinCCAL.

Example

As an example we will show a concurrent counter can be implemented in terms of a lock and register.

Module LinCCALExample.
  Import (coercions, canonicals) Sig.

  Variant spec_action {E X} {m : Sig.op E} :=
    | stop
    | scont (n : Sig.ar m) (x : X).

  Arguments spec_action : clear implicits.

  CoFixpoint unfold {E A} (α : A → LinCCAL.tid → ∀ m, spec_action E A m)
    (x : A) (t : LinCCAL.TMap.key) (m : Sig.op E) : LinCCAL.spec_after E m :=
    match α x t m with
      | stop ⇒ LinCCAL.spec_top
      | scont n y ⇒ LinCCAL.spec_cons n (unfold α y)
    end.

  Lemma spec_unfold {E q} (σ : LinCCAL.spec_after E q) :
    σ =
    match σ with
      | LinCCAL.spec_top ⇒ LinCCAL.spec_top
      | LinCCAL.spec_cons n σ' ⇒ LinCCAL.spec_cons n σ'
    end.

  Lemma unfold_unfold {E A} α x t m :
    @unfold E A α x t m =
    match α x t m with
      | stop ⇒ LinCCAL.spec_top
      | scont n y ⇒ LinCCAL.spec_cons n (unfold α y)
    end.

  Notation "% e" := (Sig.mkop e).

Counter specification


  Variant Ecounter_op :=
    | fai.

  Canonical Structure Ecounter :=
    {|
      Sig.op := Ecounter_op;
      Sig.ar _ := nat;
    |}.

  Definition Σcounter : nat → LinCCAL.spec Ecounter :=
    unfold (fun c t 'fai ⇒ scont (m:=fai) c (S c)).

  Definition Lcounter : LinCCAL.t :=
    {| LinCCAL.li_spec := Σcounter 0; |}.

Lock specification


  Variant Elock_op :=
    | acq
    | rel.

  Canonical Structure Elock :=
    {|
      Sig.op := Elock_op;
      Sig.ar _ := unit;
    |}.

  Definition Σlock (s : option LinCCAL.tid) t m : spec_action _ (option LinCCAL.tid) m :=
    (* XXX need to compare thread id's and use ⊥ where appropriate *)
    match s, m with
    | None, acq ⇒ scont (m:=acq) tt (Some t)
    | None, rel ⇒ scont (m:=rel) tt None
    | Some i, acq ⇒ stop
    | Some i, rel ⇒ scont (m:=rel) tt None
    end.

  Definition Llock : LinCCAL.t :=
    {| LinCCAL.li_spec := unfold Σlock None |}.

Register specification


  Variant Ereg_op {S} :=
    | get
    | set (s : S).

  Arguments Ereg_op : clear implicits.

  Canonical Structure Ereg S :=
    {|
      Sig.op := Ereg_op S;
      Sig.ar m := match m with
                    | get ⇒ S
                    | set _ ⇒ unit
                  end;
    |}.

  Definition Σreg S :=
    unfold (A:=S) (fun s t m ⇒
      match m with
        | get ⇒ scont (m:=get) s s
        | set s' ⇒ scont (m:=set _) tt s'
      end).

  Definition Lreg {S} (s0 : S) :=
    {| LinCCAL.li_spec := Σreg S s0 |}.

Horizontal composition (TODO: generalize)


  Canonical Structure Sig_plus (E F : Sig.t) : Sig.t :=
    {|
      Sig.op := Sig.op E + Sig.op F;
      Sig.ar := sum_rect _ Sig.ar Sig.ar;
    |}.

  Infix "+" := Sig_plus.

  Definition spec_mix {E1 E2} :=
    unfold (E := E1 + E2) (A := LinCCAL.spec E1 × LinCCAL.spec E2)
      (fun Σ t m ⇒
         match m with
           | inl m1 ⇒ match fst Σ t m1 with
                         | LinCCAL.spec_top ⇒ stop
                         | LinCCAL.spec_cons n Σ1 ⇒ scont (m := inl m1) n (Σ1, snd Σ)
                       end
           | inr m2 ⇒ match snd Σ t m2 with
                         | LinCCAL.spec_top ⇒ stop
                         | LinCCAL.spec_cons n Σ2 ⇒ scont (m := inr m2) n (fst Σ, Σ2)
                       end
         end).

  Definition tens (L1 L2 : LinCCAL.t) : LinCCAL.t :=
    {| LinCCAL.li_spec := spec_mix (LinCCAL.li_spec L1, LinCCAL.li_spec L2) |}.

  Infix "×" := tens.

Implementation


  Import (notations) Sig.
  Import (notations) LinCCAL.
  Open Scope term_scope.

  Definition fai_impl : Sig.term (LinCCAL.li_sig (Llock × Lreg 0)) nat :=
    inl acq ≥ _ ⇒
    inr get ≥ c ⇒
    inr (set (S c)) ≥ _ ⇒
    inl rel ≥ _ ⇒
    Sig.var c.

  Variant fai_threadstate (i : LinCCAL.tid) h : _ → _ → Prop :=
    | fai_rdy c :
      h ≠ Some i →
      fai_threadstate i h c None
    | fai_acq c :
      h ≠ Some i →
      fai_threadstate i h c (Some (LinCCAL.mkts fai fai_impl None))
    | fai_get c :
      h = Some i →
      fai_threadstate i h c
        (Some (LinCCAL.mkts fai (inr get ≥ c ⇒
                                 inr (set (S c)) ≥ _ ⇒
                                 inl rel ≥ _ ⇒
                                 Sig.var c) None))
    | fai_set c :
      h = Some i →
      fai_threadstate i h c
        (Some (LinCCAL.mkts fai (inr (set (S c)) ≥ _ ⇒
                                 inl rel ≥ _ ⇒
                                 Sig.var c) None))
    | fai_rel c :
      h = Some i →
      fai_threadstate i h (S c)
        (Some (LinCCAL.mkts fai (inl rel ≥ _ ⇒
                                 Sig.var c) (Some c)))
    | fai_ret c c' :
      h ≠ Some i →
      fai_threadstate i h c'
        (Some (LinCCAL.mkts fai (Sig.var c) (Some c))).

  Variant fai_state : _ → Prop :=
    fai_state_intro h c s :
      (∀ i, fai_threadstate i h c (LinCCAL.TMap.find i s)) →
      fai_state (LinCCAL.mkst (Σcounter c) s (spec_mix (unfold Σlock h, Σreg _ c))).

  Lemma fai_threadstate_convert i h h' c c' s :
    fai_threadstate i h c s →
    h ≠ Some i →
    h' ≠ Some i →
    fai_threadstate i h' c' s.

  Program Definition Mcounter : Llock × Lreg 0 ~~> Lcounter :=
    {| LinCCAL.li_impl 'fai := fai_impl |}.

End LinCCALExample.