m_cas.ml

open Ddsv

type shared_vars = {
    m : int;
    t1 : int;
    t2 : int;
}

let show_sv r =
  Printf.sprintf "m=%d t1=%d t2=%d" r.m r.t1 r.t2

let r0 = { m = 0; t1 = 0; t2 = 0 }

let process_P = [
    ("P0", [("P.CAS", "P1", (fun r -> true),
             (fun r -> { r with m = 1; t1 = r.m }))]);
    ("P1", [("P.retry", "P0", (fun r -> r.t1 = 1),
             (fun r -> { r with t1 = 0 }));
            ("P.begin", "P2", (fun r -> r.t1 = 0),
             (fun r -> r))]);
    ("P2", [("P.end", "P3", (fun r -> true),
             (fun r -> r))]);
    ("P3", [("P.unlock", "P0", (fun r -> true),
             (fun r -> { r with m = 0 }))]);
  ]

let process_Q = [
    ("Q0", [("Q.CAS", "Q1", (fun r -> true),
             (fun r -> { r with m = 1; t2 = r.m }))]);
    ("Q1", [("Q.retry", "Q0", (fun r -> r.t2 = 1),
             (fun r -> { r with t2 = 0 }));
            ("Q.begin", "Q2", (fun r -> r.t2 = 0),
             (fun r -> r))]);
    ("Q2", [("Q.end", "Q3", (fun r -> true),
             (fun r -> r))]);
    ("Q3", [("Q.unlock", "Q0", (fun r -> true),
             (fun r -> { r with m = 0 }))]);
  ]

let ps = [process_P; process_Q]

let () =
  viz_process "m_cas_P" process_P;
  viz_process "m_cas_Q" process_Q;
  let lts = concurrent_composition r0 ps in
  lts_print_deadlocks stdout show_sv lts;
  viz_lts "m_cas" show_sv lts