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 interfaces.Functor.
Require Import interfaces.MonoidalCategory.
Require Import models.EffectSignatures.

Linearization-based Concurrent Certified Abstraction Layers


Module LinCCALBase <: Category.

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

Concurrent object specifications


  Module Spec.

Definition

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 (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 (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.

    Variant outcome {E : Sig.t} {X : Type} {m : Sig.op E} :=
      | bot
      | top
      | ret (n : Sig.ar m) (x : X).

    Arguments outcome : clear implicits.

Our specifications give an outcome of this kind for every possible thread and operation of E.

    CoInductive t {E} :=
      {
        next : tid → ∀ m, outcome E (@t E) m;
      }.

    Arguments t : clear implicits.

State-based representations

More generally, behaviors of this kind can be described by transition systems with the same shape as next.

    Notation lts E A := (A → tid → ∀ m, outcome E A m).

In fact, next constitutes a final coalgebra over specifications, meaning that states in any transition system can be mapped to specifications with the same behavior.

    CoFixpoint gen {E A} (α : lts E A) x : t E :=
      {| next t m := match α x t m with
                     | bot ⇒ bot
                     | top ⇒ top
                     | ret n y ⇒ ret n (gen α y)
                     end |}.

Tensor product


    Import (canonicals) Sig.Plus.

    Definition tens_lts {E1 E2} : lts (Sig.Plus.omap E1 E2) (t E1 × t E2) :=
      fun Σ t m ⇒
        match m with
        | inl m1 ⇒ match next (fst Σ) t m1 with
                    | bot ⇒ bot
                    | top ⇒ top
                    | ret n Σ1 ⇒ ret (m := inl m1) n (Σ1, snd Σ)
                    end
        | inr m2 ⇒ match next (snd Σ) t m2 with
                    | bot ⇒ bot
                    | top ⇒ top
                    | ret n Σ2 ⇒
                        ret (m := inr m2) n (fst Σ, Σ2)
                    end
        end.

    Definition tens {E1 E2} (Σ1 : t E1) (Σ2 : t E2) :=
      gen tens_lts (Σ1, Σ2).

  End Spec.

  Notation spec := Spec.t.

  Declare Scope spec_scope.
  Delimit Scope spec_scope with spec.
  Bind Scope spec_scope with Spec.t.
  Infix "×" := Spec.tens : spec_scope.

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) →
        Spec.next Σ t m = Spec.ret 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) →
        Spec.next Δ t q = Spec.ret r Δ' →
        TMap.add t (mkts q T (Some r)) s = s' →
        lstep (mkst Δ s Σ) (mkst Δ' s' Σ).

In addition, if it is possible for a commit to trigger an undefined behavior in the overlay specification, then any implementation behavior would be correct from this point on, so we need to relax any further correctness constraints. The following predicate identifies states for which that is not the case.

  Definition specified {E F} (s : state E F) :=
    ∀ t q T,
      TMap.find t s = Some (mkts q T None) →
      Spec.next (st_spec s) t q ≠ Spec.bot.

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) →
        Spec.next Δ t q = Spec.ret 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 :
        specified s →
        ∀ i, threadstate_valid (TMap.find i s);
      correct_safe :
        specified s →
        ∀ i q m k R,
          TMap.find i s = Some (mkts q (Sig.cons m k) R) →
          Spec.next (st_base s) i m ≠ Spec.bot;
      correct_next :
        specified s →
        ∀ 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 → specified s →
        ∀ i, threadstate_valid (TMap.find i s);
      ci_safe s :
        P s → specified s →
        ∀ i q m k R,
          TMap.find i s = Some (mkts q (Sig.cons m k) R) →
          Spec.next (st_base s) i m ≠ Spec.bot;
      ci_next s :
        P s → specified 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) Σ.

Vertical 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).

Basic properties.

    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.

    Lemma comp_tmap_specified_l w Δ s1 Γ s2 Σ s12 :
      comp_tmap w s12 s1 s2 →
      specified (mkst Δ s12 Σ) →
      specified (mkst Δ s1 Γ).

    Lemma comp_tmap_specified_r w Δ s1 Γ s2 Σ s12 :
      comp_tmap w s12 s1 s2 →
      correct M (mkst Δ s1 Γ) →
      specified (mkst Δ s12 Σ) →
      specified (mkst Γ 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 →
      specified (mkst Δ s12 Σ) →
      ∃ Δ' Γ' s12' s1' s2',
        star lstep (mkst Δ s12 Σ) (mkst Δ' s12' Σ) ∧
        (specified (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_def 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_def w (mkst Δ s12 Σ).

    Definition comp_state w s :=
      specified s → comp_state_def w s.

    Lemma comp_specified_sufficient w s :
      (specified s → reachable lstep (comp_state w) s) →
      reachable lstep (comp_state w) s.

    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) : m L1 L3 :=
    {| 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 LinCCALBase.

Horizontal composition


Module Type LinCCALTensSpec.
  Include LinCCALBase.
End LinCCALTensSpec.

Module LinCCALTens (B : LinCCALTensSpec) <: Monoidal B.
  Import (notations, canonicals) Reg.Plus.
  Import B.
  Obligation Tactic := intros.

  Module Tens <: MonoidalStructure B.

Tensor product of layer interfaces

Two certified abstraction layers can be composed horizontally by taking method implementations as defined in Reg.Plus. Then the specification of the composite layer can be computed by independently interleaving the specifications from each side per Spec.tens, as shown below.

    Definition omap (L1 L2 : t) : t :=
      {|
        li_sig := Reg.Plus.omap (li_sig L1) (li_sig L2);
        li_spec := li_spec L1 × li_spec L2;
      |}.


Tensor product of layer implementations

For some reason, congruence and other tactics are buggy when faced with those cases.

    Lemma inj_somets2 {E F} q T1 T2 R1 R2 :
      Some (@mkts E F q T1 R1) = Some (@mkts E F q T2 R2) →
      T1 = T2 ∧ R1 = R2.

Owing to proof irrelevance, the monoidal structure associated with the tensor product of layers can be pulled from Reg.Plus. However, we first need to prove locality and show that horizontal composition preserves layer correctness. Fortunately, because the two layer act largely independently from each other, this is much simpler to establish than the vertical composition property used to define compose

    Section CORRECTNESS.
      Context {E1 E2 F1 F2 : Sig.t}.
      Context (M1 : Reg.Op.m E1 F1).
      Context (M2 : Reg.Op.m E2 F2).

Per-thread invariant

      Variant fmap_threadstate : _ → _ → _ → Prop :=
        | fmap_ts_none :
          fmap_threadstate
            None
            None
            None
        | fmap_ts_left (q : Sig.op F1) (T : Sig.term E1 (Sig.ar q)) R :
          fmap_threadstate
            (Some (mkts (inl q) (Reg.transform Reg.Plus.i1 T) R))
            (Some (mkts q T R))
            None
        | fmap_ts_right (q : Sig.op F2) (T : Sig.term E2 (Sig.ar q)) R :
          fmap_threadstate
            (Some (mkts (inr q) (Reg.transform Reg.Plus.i2 T) R))
            None
            (Some (mkts q T R)).

Thread map invariant

      Definition fmap_tmap (s12 s1 s2 : tmap _) :=
        ∀ i,
          fmap_threadstate (TMap.find i s12) (TMap.find i s1) (TMap.find i s2).

      Lemma fmap_tmap_specified_l Σ1 Σ2 s12 s1 s2 Δ1 Δ2 :
        fmap_tmap s12 s1 s2 →
        specified (mkst (Σ1 × Σ2) s12 (Δ1 × Δ2)) →
        specified (mkst Σ1 s1 Δ1).

      Lemma fmap_tmap_specified_r Σ1 Σ2 s12 s1 s2 Δ1 Δ2 :
        fmap_tmap s12 s1 s2 →
        specified (mkst (Σ1 × Σ2) s12 (Δ1 × Δ2)) →
        specified (mkst Σ2 s2 Δ2).

Global state invariant

      Variant fmap_state : state _ _ → Prop :=
        fmap_state_intro s12 s1 s2 Δ1 Δ2 Σ1 Σ2 :
          fmap_tmap s12 s1 s2 →
          correct M1 (mkst Δ1 s1 Σ1) →
          correct M2 (mkst Δ2 s2 Σ2) →
          fmap_state (mkst (Δ1 × Δ2) s12 (Σ1 × Σ2)).

      Lemma fmap_lsteps_l s12 s1 s2 Δ1 Δ2 Σ1 Σ2 :
        fmap_tmap s12 s1 s2 →
        reachable lstep (correct M1) (mkst Δ1 s1 Σ1) →
        correct M2 (mkst Δ2 s2 Σ2) →
        reachable lstep fmap_state (mkst (Δ1 × Δ2) s12 (Σ1 × Σ2)).

      Lemma fmap_lsteps_r s12 s1 s2 Δ1 Δ2 Σ1 Σ2 :
        fmap_tmap s12 s1 s2 →
        correct M1 (mkst Δ1 s1 Σ1) →
        reachable lstep (correct M2) (mkst Δ2 s2 Σ2) →
        reachable lstep fmap_state (mkst (Δ1 × Δ2) s12 (Σ1 × Σ2)).

      Lemma fmap_ci :
        correctness_invariant (Reg.Plus.fmap M1 M2) fmap_state.
    End CORRECTNESS.

    Program Definition fmap {L1 L2 L1' L2'} (M1: L1~~>L1') (M2: L2~~>L2') :
      L1 × L2 ~~> L1' × L2' :=
        {| li_impl := Reg.Plus.fmap (li_impl M1) (li_impl M2) |}.


Functoriality


    Theorem fmap_id E1 E2 :
      fmap (id E1) (id E2) = id (omap E1 E2).

    Theorem fmap_compose {E1 E2 F1 F2 G1 G2} :
      ∀ (g1: F1 ~~> G1) (g2: F2 ~~> G2) (f1: E1 ~~> F1) (f2: E2 ~~> F2),
        fmap (g1 @ f1) (g2 @ f2) = fmap g1 g2 @ fmap f1 f2.

Zero layer interface

The empty spec is used to define the zero layer interface.

    Definition unit :=
      {|
        li_sig := Reg.Plus.unit;
        li_spec := Spec.gen (fun _ _ ⇒ Empty_set_rect _) tt;
      |}.

Structural isomorphisms

As with fmap, we must show that the various structural isomorphisms constitute correct layer implementations. This is tedious but mostly straightforward. In order to streamline the process somewhat we define a generic correctness invariant induced by a Sig.morphism, which generalizes the correctness invariant we used for LinCCAL.id.

    Section ISO_CORRECTNESS.
      Context {E F} (ϕ : Sig.Op.m E F).
      Import (notations) Sig.

      Variant iso_threadstate : threadstate E F → Prop :=
        | iso_invoked q :
          iso_threadstate (mkts q (Sig.operator (ϕ q) ≥ n ⇒
                                   Sig.var (Sig.operand (ϕ q) n)) None)
        | iso_returned q n :
          iso_threadstate (mkts q (Sig.var (Sig.operand (ϕ q) n))
                                     (Some (Sig.operand (ϕ q) n))).

      Definition iso_tmap (s : tmap (threadstate E F)) :=
        ∀ t st, TMap.find t s = Some st → iso_threadstate st.

    End ISO_CORRECTNESS.

Unfortunately the overall invariant still must be defined on a case-by-case basis, because the way the spec components of the parameters are involved varies from one to the next.


    Variant assoc_fw_state {E F G}: state _ _ → Prop :=
      | assoc_fw_state_intro Σ Φ Γ s :
        iso_tmap (Sig.bw (Sig.Plus.assoc E F G)) s →
        assoc_fw_state (mkst ((Σ × Φ) × Γ) s (Σ × (Φ × Γ))).

    Variant assoc_bw_state {E F G}: state _ _ → Prop :=
      | assoc_bw_state_intro Σ Φ Γ s :
        iso_tmap (Sig.fw (Sig.Plus.assoc E F G)) s →
        assoc_bw_state (mkst (Σ × (Φ × Γ)) s ((Σ × Φ) × Γ)).

    Program Definition assoc L1 L2 L3 : iso (L1 × (L2 × L3)) ((L1 × L2) × L3) :=
      {|
        fw := {| li_impl := Reg.bw (Reg.Plus.assoc _ _ _) |};
        bw := {| li_impl := Reg.fw (Reg.Plus.assoc _ _ _) |};
      |}.

    Variant lunit_fw_state {E}: state _ _ → Prop :=
      | lunit_fw_state_intro Σ s :
        iso_tmap (Sig.bw (Sig.Plus.lunit E)) s →
        lunit_fw_state (mkst Σ s (li_spec unit × Σ)).

    Variant lunit_bw_state {E}: state _ _ → Prop :=
      | lunit_bw_state_intro Σ s :
        iso_tmap (Sig.fw (Sig.Plus.lunit E)) s →
        lunit_bw_state (mkst (li_spec unit × Σ) s Σ).

    Program Definition lunit L : iso (unit × L) L :=
      {|
        fw := {| li_impl := Reg.bw (Reg.Plus.lunit _) |};
        bw := {| li_impl := Reg.fw (Reg.Plus.lunit _) |};
      |}.

    Variant runit_fw_state {E}: state _ _ → Prop :=
      | runit_fw_state_intro Σ s :
        iso_tmap (Sig.bw (Sig.Plus.runit E)) s →
        runit_fw_state (mkst Σ s (Σ × li_spec unit)).

    Variant runit_bw_state {E}: state _ _ → Prop :=
      | runit_bw_state_intro Σ s :
        iso_tmap (Sig.fw (Sig.Plus.runit E)) s →
        runit_bw_state (mkst (Σ × li_spec unit) s Σ).

    Program Definition runit L : iso (L × unit) L :=
      {|
        fw := {| li_impl := Reg.bw (Reg.Plus.runit _) |};
        bw := {| li_impl := Reg.fw (Reg.Plus.runit _) |};
      |}.

Naturality properties


    Theorem assoc_nat {A1 B1 C1 A2 B2 C2} f g h :
      fmap (fmap f g) h @ assoc A1 B1 C1 = assoc A2 B2 C2 @ fmap f (fmap g h).

    Theorem lunit_nat {A1 A2} f :
      f @ lunit A1 = lunit A2 @ fmap (id unit) f.

    Theorem runit_nat {A1 A2} f :
      f @ runit A1 = runit A2 @ fmap f (id unit).

Coherence diagrams


    Theorem assoc_coh A B C D :
      fmap (assoc A B C) (id D) @
        assoc A (omap B C) D @
        fmap (id A) (assoc B C D) =
      assoc (omap A B) C D @
        assoc A B (omap C D).

    Theorem unit_coh A B :
      fmap (runit A) (id B) @ assoc A unit B = fmap (id A) (lunit B).

    Include BifunctorTheory B B B.
    Include MonoidalStructureTheory B.
  End Tens.

  Include MonoidalTheory B.
End LinCCALTens.

Putting everything together


Module LinCCAL <: MonoidalCategory :=
  LinCCALBase <+
  LinCCALTens.

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, notations) Sig.
  Open Scope term_scope.

Counter specification


  Variant Ecounter_op :=
    | fai.

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

  Definition Σcounter : LinCCAL.Spec.lts Ecounter nat :=
    fun c t 'fai ⇒ LinCCAL.Spec.ret (m:=fai) c (S c).

  Definition Lcounter : LinCCAL.t :=
    {| LinCCAL.li_spec := LinCCAL.Spec.gen Σcounter 0%nat; |}.

Lock specification


  Variant Elock_op :=
    | acq
    | rel.

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

  Definition Σlock : LinCCAL.Spec.lts Elock (option LinCCAL.tid) :=
    fun s t m ⇒
      match s, m with
      | None, acq ⇒ LinCCAL.Spec.ret (m:=acq) tt (Some t)
      | None, rel ⇒ LinCCAL.Spec.bot
      | Some i, acq ⇒
          if LinCCAL.TMap.E.eq_dec i t then LinCCAL.Spec.bot
                                       else LinCCAL.Spec.top
      | Some i, rel ⇒
          if LinCCAL.TMap.E.eq_dec i t then LinCCAL.Spec.ret (m:=rel) tt None
                                       else LinCCAL.Spec.bot
      end.

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

Register specification


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

  Arguments Ereg_op : clear implicits.

  Definition Ereg_ar {S} (m : Ereg_op S) :=
    match m with
      | get ⇒ S
      | set _ ⇒ unit
    end.

  Canonical Structure Ereg S :=
    {|
      Sig.op := Ereg_op S;
      Sig.ar := Ereg_ar;
    |}.

  Definition Σreg S : LinCCAL.Spec.lts (Ereg S) S :=
    fun s t m ⇒
      match m with
        | get ⇒ LinCCAL.Spec.ret (m:=get) s s
        | set s' ⇒ LinCCAL.Spec.ret (m:=set _) tt s'
      end.

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

Implementation


  Import (notations) LinCCAL.
  Import (canonicals) Sig.Plus.

  Definition fai_impl : Sig.term (LinCCAL.li_sig (Llock × Lreg 0%nat)%obj) 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 (LinCCAL.Spec.gen Σcounter c)
                              s
                              (LinCCAL.Spec.gen Σlock h ×
                               LinCCAL.Spec.gen (Σ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 : LinCCAL.m (Llock × Lreg 0%nat) Lcounter :=
    {| LinCCAL.li_impl 'fai := fai_impl |}.

End LinCCALExample.