Litmus

LeanCats.lean

@@ -1,3 +1,18 @@
 -- This module serves as the root of the `LeanCats` library.
 -- Import modules here that should be built as part of the library.
+import LeanCats.Data
+import LeanCats.HashMapExt
+import LeanCats.Relations
 import LeanCats.Basic
+import LeanCats.Syntax
+import LeanCats.CatPreprocessor
+import LeanCats.Macro
+import LeanCats.Theorems
+import LeanCats.TsoWeakerThanSc
+import LeanCats.ModelReader
+import LeanCats.Litmus
+import LeanCats.LitmusParser
+import LeanCats.LitmusGraph
+import LeanCats.LitmusGraphBridge
+import LeanCats.LitmusReader
+import LeanCats.Linux.CoRR_poonceonce_Once

LeanCats/Basic.lean

@@ -8,15 +8,59 @@ open CatRel
 This definination is different with the formal semantics, because the `co` is defined in [stdlib.cat](https://github.com/herd/herdtools7/blob/2a7599f8ecdbde0ed67925daf6534c1a0c26d535/herd-www/cat_includes/stdlib.cat) and
 by computation, so should declare it as the base relation. -/
 structure CandidateExecution (evts : Events) where
+  evts := evts
   idUnique := ∀ e₁ e₂ : Event, (e₁ ∈ evts ∧ e₂ ∈ evts) -> e₁.id ≠ e₂.id
-  po   := evts.po
-  rf   : SetRel Event Event
-  rfInst : wellformed.rf evts rf
-  co   : SetRel Event Event
-  [preCo : wellformed.co evts co]
-  fr   := rf.inv.comp co
-  rmw  : SetRel Event Event
+  po'   := evts.po
+  [prePo: wellformed.po po']
+  rf'   : SetRel Event Event := ∅
+  rfInst : wellformed.rf evts rf'
+  co'   : SetRel Event Event := ∅
+  [preCo : wellformed.co evts co']
+  rmw'  : SetRel Event Event := ∅
+  [preRMW : wellformed.rmw evts rmw']
+  wmb'  : SetRel Event Event := ∅
+  data' : SetRel Event Event := ∅
+  addr' : SetRel Event Event := ∅
+  ctrl' : SetRel Event Event := ∅
+  fence' : SetRel Event Event := ∅
+  mb' : SetRel Event Event := ∅
   uniqueId : ∀ (e₁ e₂ : Event),
     e₁ ∈ evts.all → e₂ ∈ evts.all
     -> e₁ ≠ e₂
     → e₁.id ≠ e₂.id
+  -- Internal reads-from implies program order: if a write and its read
+  -- are on the same thread, the write must precede the read in po.
+  rfiPo : ∀ (w r : Event),
+    (w, r) ∈ rf'
+    → w.t_id = r.t_id
+    → (w, r) ∈ evts.po
+  coWR : ∀ (w r w' : Event),
+    (w, r) ∈ evts.po
+    → w.effect.location = r.effect.location
+    → (w', r) ∈ rf'
+    → (w, w') ∈ co' ∨ w = w'
+
+/-- from-reads: always defined as rf⁻¹ ; co, so it is transparent to the kernel. -/
+@[simp] def CandidateExecution.fr' {evts : Events} (X : CandidateExecution evts) : SetRel Event Event :=
+  X.rf'.inv.comp X.co'
+
+/-- The `uniqueId` field of any `CandidateExecution`: since `event_id_unique` makes identity
+    determined solely by ID, any two distinct events must have distinct IDs. -/
+theorem uniqueId_by_id (evts : Events) :
+    ∀ (e₁ e₂ : Event), e₁ ∈ evts.all → e₂ ∈ evts.all → e₁ ≠ e₂ → e₁.id ≠ e₂.id :=
+  fun _ _ _ _ hne hid => hne (Data.event_id_unique _ _ hid)
+
+/-- Tactic for proving the `rfiPo` and `coWR` obligations of a `CandidateExecution`
+    for concrete litmus tests with finite event sets.
+
+    Strategy: unfold all set memberships with standard `Set` simp lemmas plus any
+    user-supplied lemmas (typically the `co` and `evts` `@[simp]` definitions), then
+    close by `omega` (handles numeric contradictions on IDs / thread IDs) with
+    `simp_all` as a pre-processing step when `omega` alone is insufficient. -/
+macro "candidateExecution_wf" : tactic =>
+  `(tactic|
+    (all_goals repeat first
+       | simp at *
+         aesop
+       | (casesm _ ∈ _
+          aesop)))

LeanCats/CatPreprocessor.lean

@@ -1,4 +1,6 @@
 
+import Std.Data.HashMap
+
 namespace String
 @[specialize]
 def foldl2Aux {α : Type u} (f : α → Char → Char → α) (s : String) (stopPos : Pos.Raw) (i : Pos.Raw) (a : α) : α :=
@@ -58,27 +60,119 @@ private def processHead (accDone : String × Bool)  : Char → String × Bool :=
     | '"' => (acc, true)
     | _ => (acc, false)
 
+private def isCatIdentChar (c : Char) : Bool :=
+  c.isAlphanum || c == '_' || c == '-'
+
+private structure TickRewriteState where
+  acc : String := ""
+  tok : String := ""
+  pendingTick : Bool := false
+
+private def flushTickState (st : TickRewriteState) : TickRewriteState :=
+  if st.tok.isEmpty then
+    if st.pendingTick then
+      { acc := st.acc.push '\'', tok := "", pendingTick := false }
+    else
+      st
+  else
+    let acc :=
+      if st.pendingTick then st.acc ++ st.tok ++ "'"
+      else st.acc ++ st.tok
+    { acc := acc, tok := "", pendingTick := false }
+
+/-- Rewrite CAT tick-prefixed identifiers from `'TAG` to `TAG'`. -/
 def removeFrontTick (input : String) : String :=
-  (input.splitOn.map (fun s => s.stripPrefix "\'")) |> (String.intercalate " ")
-  |>.splitOn "\n" |>.map (fun s => s.stripPrefix "\'") |> (String.intercalate "\n")
-  |>.splitOn "\t" |>.map (fun s => s.stripPrefix "\'") |> (String.intercalate " ")
+  let st := input.toList.foldl (fun st c =>
+    if isCatIdentChar c then
+      { st with tok := st.tok.push c }
+    else if c == '\'' then
+      if st.tok.isEmpty then
+        if st.pendingTick then
+          { acc := st.acc.push '\'', tok := "", pendingTick := true }
+        else
+          { st with pendingTick := true }
+      else
+        { acc := st.acc ++ st.tok ++ "'", tok := "", pendingTick := false }
+    else
+      let st := flushTickState st
+      { st with acc := st.acc.push c }
+  ) {}
+  (flushTickState st).acc
 
 def removeTickAndCapitalize (s : String) : String :=
-  let stripped := (s.dropPrefix "\'").toString
+  let stripped := (s.dropPrefix "\'").toString ++ "'"
   if stripped.isEmpty then
     stripped
   else
     let firstChar := String.Pos.Raw.get stripped ⟨0⟩
     let rest := stripped.drop 1
     (firstChar.toUpper.toString ++ rest)
 
+private structure InstrGroup where
+  firstIdx : Nat
+  events   : Array String
+
+private def parseInstructionsLine? (line : String) : Option (Array String × String) :=
+  let trimmed := (String.trimAscii line).toString
+  if !(trimmed.startsWith "instructions ") then
+    none
+  else
+    let rest := (String.dropPrefix trimmed "instructions ").toString
+    match rest.splitOn "[" with
+    | [evtsRaw, tagsAndTail] =>
+      match tagsAndTail.splitOn "]" with
+      | [] => none
+      | tag::_ =>
+        let eventText := (String.trimAscii evtsRaw).toString
+        let events :=
+          if eventText.startsWith "{" && eventText.endsWith "}" then
+            let body := ((eventText.drop 1).dropEnd 1).toString
+            (body.splitOn ",").map (fun s => (String.trimAscii s).toString) |>.toArray
+          else
+            #[eventText]
+        let tagTrimmed := (String.trimAscii tag).toString
+        if events.isEmpty || tagTrimmed.isEmpty then none
+        else some (events, tagTrimmed)
+    | _ => none
+
+private def mergeInstructionTagLines (input : String) : String := Id.run do
+  let lines := input.splitOn "\n"
+  let mut groups : Std.HashMap String InstrGroup := {}
+
+  for i in [:lines.length] do
+    let line := lines[i]!
+    match parseInstructionsLine? line with
+    | none => pure ()
+    | some (events, tag) =>
+      match groups.get? tag with
+      | none =>
+        groups := groups.insert tag { firstIdx := i, events := events }
+      | some g =>
+        let merged := events.foldl (fun acc e => if acc.contains e then acc else acc.push e) g.events
+        groups := groups.insert tag { g with events := merged }
+
+  let mut out : List String := []
+  for i in [:lines.length] do
+    let line := lines[i]!
+    match parseInstructionsLine? line with
+    | none => out := line :: out
+    | some (_, tag) =>
+      match groups.get? tag with
+      | some g =>
+        if g.firstIdx == i then
+          let mergedEvts := String.intercalate ", " g.events.toList
+          out := ("instructions {" ++ mergedEvts ++ "}[" ++ tag ++ "]") :: out
+      | none => out := line :: out
+
+  String.intercalate "\n" out.reverse
+
 def removeComments (input : String) : String :=
   let removedTick := removeFrontTick input
   let headProcessed : String := match removedTick.toList with
     | [] => .ofList []
     | '"'::rest => (String.ofList rest).foldl processHead (String.ofList [], false) |>.1
     | s => .ofList s
-  removeBlockComments headProcessed
+  mergeInstructionTagLines (removeBlockComments headProcessed)
 
 #eval removeFrontTick "'example || 'string"
 
@@ -112,9 +206,13 @@ def Filename.mkName (inp : String) : Lean.Name := Id.run do
 
 
 def enums_test := "enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) ||
-		'RELEASE (*smp_store_release*) ||
+		'Release (*smp_store_release*) ||
 		'ACQUIRE (*smp_load_acquire*) ||
 		'NORETURN (* R of non-return RMW *) ||
 		'MB (*xchg(),cmpxchg(),...*)"
 
 #eval removeComments enums_test
+
+def instructions_test := "instructions R[Accesses]\ninstructions W[Accesses]\ninstructions RMW[Accesses]\ninstructions F[Barriers]"
+
+#eval removeComments instructions_test

LeanCats/Cats/examples/models/lkmm.bell

@@ -0,0 +1,49 @@
+(*
+ * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
+ * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
+ * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
+ *                    Andrea Parri <parri.andrea@gmail.com>
+ *
+ * An earlier version of this file appeared in the companion webpage for
+ * "Frightening small children and disconcerting grown-ups: Concurrency
+ * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
+ * which appeared in ASPLOS 2018.
+ *)
+
+enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) ||
+		'RELEASE (*smp_store_release*) ||
+		'ACQUIRE (*smp_load_acquire*) ||
+		'NORETURN (* R of non-return RMW *) ||
+		'MB (*xchg(),cmpxchg(),...*)
+instructions R[Accesses]
+instructions W[Accesses]
+instructions RMW[Accesses]
+
+enum Barriers = 'wmb (*smp_wmb*) ||
+		'rmb (*smp_rmb*) ||
+		'MB (*smp_mb*) ||
+		'barrier (*barrier*) ||
+		'rcu-lock (*rcu_read_lock*)  ||
+		'rcu-unlock (*rcu_read_unlock*) ||
+		'sync-rcu (*synchronize_rcu*) ||
+		'before-atomic (*smp_mb__before_atomic*) ||
+		'after-atomic (*smp_mb__after_atomic*) ||
+		'after-spinlock (*smp_mb__after_spinlock*) ||
+		'after-unlock-lock (*smp_mb__after_unlock_lock*) ||
+		'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
+instructions F[Barriers]
+
+(*
+ * Filter out syntactic annotations that do not provide the corresponding
+ * semantic ordering, such as Acquire on a store or Mb on a failed RMW.
+ *)
+let FailedRMW = RMW \ (domain(rmw) | range(rmw))
+let Acquire = ACQUIRE \ W \ FailedRMW
+let Release = RELEASE \ R \ FailedRMW
+let Mb = MB \ FailedRMW
+let Noreturn = NORETURN \ W
+
+(* Compute marked and plain memory accesses *)
+let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW |
+		LKR | LKW | UL | LF | RL | RU
+let Plain = M \ Marked