Artifact for POPL 2024 submission

Author: Twisol

Clock/Classifier.agda

@@ -0,0 +1,85 @@
+{-# OPTIONS --safe --without-K --exact-split --no-import-sorts #-}
+open import Agda.Primitive
+  using () renaming (Set to Type)
+open import Relation.Binary
+  using (DecidableEquality)
+
+{-
+  A clock that classifies actions and tracks a lower bound on
+  the number of actions occurring in each class.
+
+  `Act` is the type of actions that can be performed.
+  `Cls` is the type of action classes.
+  Every `Act` is assigned to a `Cls` by the `cls` classification function.
+  `_≟_` decides if two classes are the same.
+
+  Special cases:
+  - The scalar clock of Lamport, which has only one classification.
+  - The vector clock of Mattern, and of Fidge, which classifies actions
+    by who performed them.
+  - The matrix clock of Sarin and Lynch, and of Raynal and Singhal, which
+    classifies actions by a tuple of sender and recipient.
+-}
+module Clock.Classifier
+    (Cls : Type) (_≟_ : DecidableEquality Cls)
+    (Act : Type) (cls : Act → Cls)
+  where
+  open import Data.Bool
+    using (true; false)
+  open import Data.Nat
+    using (ℕ; _+_; _⊔_; _≤_)
+  open import Data.Nat.Properties
+    as ℕ-Prop
+    using ()
+  open import Data.Bool
+    using (if_then_else_)
+  open import Relation.Nullary
+    using (does; _because_)
+
+  open import Clock.Interpret
+    as Interpret
+    using (Step; act; merge)
+  open import Clock.Monotonicity
+    as Monotonicity
+    using (Clock)
+  open Clock
+    using (≤-refl; ≤-trans; act-mono; merge-mono¹; merge-mono²)
+
+  -- A timestamp is a count of actions for every action class.
+  Time : Type
+  Time = Cls → ℕ
+
+  alg : Step Act Time → Time
+  -- The increment operation adds one to the class of the associated action.
+  alg (act a t) = λ c →
+    if does (cls a ≟ c)
+      then 1 + t c
+      else 0 + t c
+  -- The merge operation takes the pointwise least upper bound
+  -- (i.e. separately for each class).
+  -- Notice that we cannot simply *add* the counts, because some actions
+  -- might then be double-counted. Instead, if one clock has observed
+  -- five actions, and another has observed seven, all we know is that
+  -- at least 7 actions have definitely occurred.
+  alg (merge t₁ t₂) = λ c →
+    t₁ c ⊔ t₂ c
+
+  -- Timestamps are ordered pointwise (i.e. separately for each class).
+  _⊑_ : Time → Time → Type
+  t₁ ⊑ t₂ = ∀ c → t₁ c ≤ t₂ c
+
+  clock : Clock alg _⊑_
+  -- _⊑_ is a preorder:
+  (≤-refl      clock) _ _   = ℕ-Prop.≤-refl
+  (≤-trans     clock) _ _ _ t₁≤t₂ t₂≤t₃ = λ s → ℕ-Prop.≤-trans (t₁≤t₂ s) (t₂≤t₃ s)
+  -- The clock operations are increasing on _⊑_:
+  (act-mono    clock) a _ s with cls a ≟ s
+  ... | false because _     = ℕ-Prop.≤-refl
+  ... | true  because _     = ℕ-Prop.≤-step ℕ-Prop.≤-refl
+  (merge-mono¹ clock) _ _ _ = ℕ-Prop.m≤m⊔n _ _
+  (merge-mono² clock) _ _ _ = ℕ-Prop.m≤n⊔m _ _
+
+  -- Obtain a global timestamping function for any execution.
+  timestamp = Interpret.timestamp alg
+  -- Obtain a proof of the clock condition for any execution and any initial timestamps.
+  mono = Monotonicity.timestamp-mono clock

Clock/Interpret.agda

@@ -0,0 +1,68 @@
+{-# OPTIONS --safe --without-K --exact-split --no-import-sorts #-}
+open import Agda.Primitive
+  using () renaming (Set to Type)
+
+module Clock.Interpret where
+  open import Function
+    using (_∘_)
+  open import Data.Sum
+    using (inj₁; inj₂)
+  open import Execution.Sites
+    as Sites
+    using (Tree; Site; _∗_)
+  open import Execution.Core
+    using (perm; tick; fork; join)
+    using (_⇶[_]_; _⇶_; id; _∥_; _⟫_)
+    using (Event; Tick)
+  open import Execution.Causality
+    as HB
+    using ()
+  open Event
+    using (_,_)
+
+  variable
+    T : Type
+    Γ Γ₁ Γ₂ Γ₃ Γ₄ : Tree (Tree T)
+    Action State : Type
+
+  Valuation : Type → Tree (Tree T) → Type
+  Valuation State Γ = Site Γ → State
+
+  par : Valuation State Γ₁ → Valuation State Γ₂ → Valuation State (Γ₁ ∗ Γ₂)
+  par f g (Site.thereˡ _ ix) = f ix
+  par f g (Site.thereʳ _ ix) = g ix
+
+  left : Valuation State (Γ₁ ∗ Γ₂) → Valuation State Γ₁
+  left f = f ∘ Site.thereˡ _
+
+  right : Valuation State (Γ₁ ∗ Γ₂) → Valuation State Γ₂
+  right f = f ∘ Site.thereʳ _
+
+  _⊗_ : (Valuation State Γ₁        → Valuation State Γ₂       )
+      → (Valuation State       Γ₃  → Valuation State       Γ₄ )
+      → (Valuation State (Γ₁ ∗ Γ₃) → Valuation State (Γ₂ ∗ Γ₄))
+  (f ⊗ g) x = par (f (left x)) (g (right x))
+
+  data Step (Action State : Type) : Type where
+    act   : Action → State → Step Action State
+    merge : State  → State → Step Action State
+
+  -- Given an algebra on steps, we can specify computations
+  -- on replicas across spatially-distributed sites.
+  module _ (alg : Step Action State → State) where
+    apply : ∀{k} (exec : Γ₁ ⇶[ k ] Γ₂) (acts : Tick exec → Action)
+          → (Valuation State Γ₁ → Valuation State Γ₂)
+    apply  id   acts   = Function.id
+    apply (perm σ) _ f = f ∘ Sites.‵index (Sites.‵sym σ)
+    apply  fork    _ f = Function.const (f Site.here)
+    apply  tick acts f = Function.const (alg (act (acts _) (f Site.here)))
+    apply  join    _ f = Function.const (alg (merge (f (Site.thereˡ _ Site.here))
+                                                    (f (Site.thereʳ _ Site.here)) ))
+    apply (  left ∥  right) acts = apply left   (acts ∘ inj₁) ⊗ apply right  (acts ∘ inj₂)
+    apply (prefix ⟫ suffix) acts = apply suffix (acts ∘ inj₂) ∘ apply prefix (acts ∘ inj₁)
+
+    timestamp : {exec : Γ₁ ⇶ Γ₂}
+              → (Tick exec → Action)
+              → Valuation State Γ₁
+              → (Event exec → State)
+    timestamp acts init (t , s) = apply (HB.before[ t ]) (acts ∘ HB.tliftˡ t) init s

Clock/Matrix.agda

@@ -0,0 +1,88 @@
+{-# OPTIONS --safe --without-K --exact-split --no-import-sorts #-}
+open import Agda.Primitive
+  using () renaming (Set to Type)
+open import Relation.Binary
+  using (DecidableEquality)
+
+module Clock.Matrix (Pid : Type) (_≟_ : DecidableEquality Pid) where
+  open import Data.Product
+    using (_×_)
+  open import Data.Product.Properties
+    using (≡-dec)
+
+  -- A Raynal-Schiper-Toueg matrix clock classifies actions by a tuple
+  -- of sender and recipient. This forms a table of quantities, one for
+  -- each sender-recipient pair.
+  --
+  -- This is *distinct* from a Wuu-Bernstein matrix clock, which has an extra
+  -- step in its merge operation to propagate knowledge of observation.
+  module RST where
+    open import Clock.Classifier (Pid × Pid) (≡-dec _≟_ _≟_) public
+      using (Time; _⊑_; alg; clock; timestamp; mono)
+
+  -- A Wuu-Bernstein matrix clock classifies actions by actor and observer.
+  -- If an action is observed by multiple actors, the action will be counted
+  -- in multiple places in the matrix. This requires not only a pointwise merge,
+  -- but also a merge of a sender's row into a receiver's row, to model that
+  -- the receiver now observes anything that the sender observed at the time
+  -- the message was sent.
+  module WB where
+    open import Data.Unit
+      using (⊤)
+    open import Data.Product
+      using (_,_)
+    open import Data.Bool
+      using (true; false)
+    open import Data.Nat
+      using (ℕ; _+_; _⊔_; _≤_)
+    open import Data.Nat.Properties
+      as ℕ-Prop
+      using ()
+    open import Data.Bool
+      using (if_then_else_)
+    open import Relation.Nullary
+      using (does; _because_)
+
+    open import Clock.Interpret
+      as Interpret
+      using (Step; act; merge)
+    open import Clock.Monotonicity
+      as Monotonicity
+      using (Clock)
+    open Clock
+      using (≤-refl; ≤-trans; act-mono; merge-mono¹; merge-mono²)
+
+    -- A local process ID, together with a timestamp.
+    Time = Pid × ((Pid × Pid) → ℕ)
+
+    -- Ignore the process ID when comparing.
+    _⊑_ : Time → Time → Type
+    (_ , t₁) ⊑ (_ , t₂) = ∀ c → t₁ c ≤ t₂ c
+
+    alg : Step ⊤ Time → Time
+    alg (act _ (self , t)) = self , λ c →
+      if does ((≡-dec _≟_ _≟_) (self , self) c)
+        then 1 + t c
+        else 0 + t c
+    alg (merge (s , t₁) (r , t₂)) = r ,  λ (i , j) →
+      if does (j ≟ r)
+        then t₁ (i , s) ⊔ (t₁ (i , j) ⊔ t₂ (i , j))
+        else 0          ⊔ (t₁ (i , j) ⊔ t₂ (i , j))
+
+    clock : Clock alg _⊑_
+    ≤-refl clock _ _ = ℕ-Prop.≤-refl
+    ≤-trans clock _ _ _ t₁≤t₂ t₂≤t₃ = λ s → ℕ-Prop.≤-trans (t₁≤t₂ s) (t₂≤t₃ s)
+    act-mono clock _ (self , _) c with (≡-dec _≟_ _≟_) (self , self) c
+    ... | false because _ = ℕ-Prop.≤-refl
+    ... | true  because _ = ℕ-Prop.≤-step ℕ-Prop.≤-refl
+    merge-mono¹ clock (s , t₁) (r , t₂) (i , j) with j ≟ r
+    ... | false because _ = ℕ-Prop.m≤m⊔n _ _
+    ... | true  because _ = ℕ-Prop.≤-trans (ℕ-Prop.m≤m⊔n _ _) (ℕ-Prop.m≤n⊔m (t₁ (i , s)) _)
+    merge-mono² clock (s , t₁) (r , t₂) (i , j) with j ≟ r
+    ... | false because _ = ℕ-Prop.m≤n⊔m _ _
+    ... | true  because _ = ℕ-Prop.≤-trans (ℕ-Prop.m≤n⊔m _ _) (ℕ-Prop.m≤n⊔m (t₁ (i , s)) _)
+
+    -- Obtain a global timestamping function for any execution.
+    timestamp = Interpret.timestamp alg
+    -- Obtain a proof of the clock condition for any execution and any initial timestamps.
+    mono = Monotonicity.timestamp-mono clock