[Proof Ground 2020] Concurrency

Definitions File

import tactic data.zmod.basic

/-
This is a specification of a simple concurrent algorithm from the paper
"Teaching Concurrency" by Leslie Lamport. In there are N processes and
two arrays of length N, x and y. Each process i executes the following
sequence of statements:
     x[i] := 1;
     y[i] := x[(i-1) mod N];
The reads and writes of each x[j] are assumed to be atomic. This
algorithm has the property that once all processes have finished, at
least one y[j] == 1.
-/

namespace concurrency

/- N is the number of processes. -/
-- variable (N : ℕ)

/- Processes are identified by natural numbers. A variable is a function
over all natural numbers, not just those from [0, N). However, the
definition of reachable below restricts updates to processes from [0, N) -/
def var (t) := ℕ → t
/- There's at least one process. -/
-- variable [fact (0 < N)]

/- Control state of a process. A process is at control
state assign_x if it has not started, assign_y if it has
executed its assignment to x but not to y, and done if it
has finished. -/
inductive pc_label
| assign_x
| assign_y
| finished
open pc_label

/- State of the system. -/
structure state :=
(pc : var pc_label)
(x  : var nat)
(y  : var nat)

def update {α} (i x) (v : var α) : var α
| j := if i = j then x else v j

@[simp]
def update_pc (st : state) (i l) : state := { pc := update i l st.pc .. st }

@[simp]
def update_x (st : state) (i v) : state := { x := update i v st.x .. st }

@[simp]
def update_y (st : state) (i v) : state := { y := update i v st.y .. st }

inductive reachable : state → Prop
| init (init_x init_y : var nat) :
  reachable { pc := (λ _, assign_x), x := init_x, y := init_y }
| x_step (st i) :
  reachable st →
  st.pc i = assign_x →
  reachable (update_x (update_pc st i assign_y) i 1)
| y_step (st i) :
  reachable st →
  st.pc i = assign_y →
  reachable (update_y (update_pc st i finished) i (st.x (i+1)))

def safe (st : state) := (∀ i, st.pc i = finished) → (∃ i, st.y i = 1)

----------------------just some definitions to prevent cheating------------------------

def reachable_safe_prop : Prop := ∀ (st : state) (h : reachable st), safe st

notation `reachable_safe_prop` := reachable_safe_prop

end concurrency

Template File

import .defs

namespace concurrency

theorem reachable_safe : ∀ (st : state) (h : reachable st), safe st :=
sorry

end concurrency

Check File

import .defs
import .submission

lemma check_reachable_safe : reachable_safe_prop := @concurrency.reachable_safe

Definitions File

Require Export Coq.Arith.PeanoNat.

Section Problem.

(* N is the number of processes. *)
Parameter N : nat.

(* Processes are identified by natural numbers. A variable is a function
over all natural numbers, not just those from [0, N). However, the
definition of reachable below restricts updates to processes from [0, N) *)
Definition var (T : Set) := nat -> T.
Definition Proc (i : nat) := i < N.
(* There's at least one process. *)
Axiom Proc_0 : Proc 0.

(* Control state of a process. A process is at control
state assign_x if it has not started, assign_y if it has
executed its assignment to x but not to y, and done if it
has finished. *)
Inductive pc_label :=
| assign_x
| assign_y
| done.

(* State of the system. *)
Record state : Set := mkState
{ pc : var pc_label
; x  : var nat
; y  : var nat
}.

(* Update the pc value of a single process *)
Definition update_pc (st : state) (i : nat) (l : pc_label) : state :=
    {|pc := fun j => if Nat.eq_dec i j then l else st.(pc) j
    ; x := st.(x)
    ; y := st.(y)|}.

(* Update the x value of a single process *)
Definition update_x (st : state) (i : nat) (v : nat) : state :=
    {|pc := st.(pc)
    ; x := fun j => if Nat.eq_dec i j then v else st.(x) j
    ; y := st.(y)|}.

(* Update the y value of a single process *)
Definition update_y (st : state) (i : nat) (v : nat) : state :=
    {|pc := st.(pc)
    ; x := st.(x)
    ; y := fun j => if Nat.eq_dec i j then v else st.(y) j|}.

(* Set of reachable states *)
Inductive reachable : state -> Prop :=
| init : forall init_x init_y, reachable
    {|pc := fun _ => assign_x; x := init_x; y := init_y |}
| x_step : forall st, reachable st ->
    forall i, Proc i -> st.(pc) i = assign_x ->
        reachable (update_x (update_pc st i assign_y) i 1)
| y_step : forall st, reachable st ->
        forall i, Proc i -> st.(pc) i = assign_y ->
            let j := if Nat.eq_dec (i + 1) N then 0 else i + 1 in
            reachable (update_y (update_pc st i done) i (st.(x) j))
.

(* Property we want to prove: if every process is done, at least
one process has y[i] = 1. *)
Definition safe st :=
    (forall i, Proc i -> st.(pc) i = done) ->
    exists i, Proc i /\ st.(y) i = 1.

End Problem.

Template File

Require Import Defs.

Theorem reachable_safe st:
    reachable st -> safe st.
Proof.
Admitted.

Definitions File

theory Defs
  imports Main
begin

(* N is the number of processes. *)
consts N :: nat

(* Processes are identified by natural numbers. A variable is a function
over all natural numbers, not just those from [0, N). However, the
definition of reachable below restricts updates to processes from [0, N) *)
type_synonym 't var = "nat \<Rightarrow> 't"
definition "Proc i \<longleftrightarrow> i < N" for i

(* There's at least one process. *)
axiomatization where proc_0: "Proc 0"

(* Control state of a process. A process is at control
state assign_x if it has not started, assign_y if it has
executed its assignment to x but not to y, and done if it
has finished. *)
datatype pc_label =
  assign_x
| assign_y
| finished

(* State of the system. *)
record state =
  pc :: "pc_label var"
  x  :: "nat var"
  y  :: "nat var"

definition
  "update_pc st i l = st\<lparr>pc := (pc st)(i := l)\<rparr>"

definition
  "update_x st i v = st\<lparr>x := (x st)(i := v)\<rparr>"

definition
  "update_y st i v = st\<lparr>y := (y st)(i := v)\<rparr>"

inductive reachable where
  init: "reachable \<lparr>pc = (\<lambda>_. assign_x), x = init_x, y = init_y\<rparr>"
| x_step: "reachable (update_x (update_pc st i assign_y) i 1)" if "reachable st" "pc st i = assign_x"
| y_step: "reachable (update_y (update_pc st i finished) i (x st ((i + 1) mod N)))"
  if "reachable st" "pc st i = assign_y"

definition safe where
  "safe st \<equiv> (\<forall>i. Proc i \<longrightarrow> pc st i = finished) \<longrightarrow> (\<exists>i. Proc i \<and> y st i = 1)"

end

Template File

theory Template
  imports Defs
begin

theorem reachable_safe :
  "safe st" if "reachable st"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem reachable_safe :
  "safe st" if "reachable st"
  using that by (rule Submission.reachable_safe)

end