m_llsc.ml

open Ddsv

type shared_vars = {
    x : int;
    t1 : int;
    t2 : int;
    a1 : int;
    a2 : int;
}

let show_sv r =
  Printf.sprintf "x=%d t1=%d t2=%d a1=%d a2=%d"
    r.x r.t1 r.t2 r.a1 r.a2

let r0 = { x = 0; t1 = 0; t2 = 0; a1 = 0; a2 = 0 }

let process_P = [
    ("P0", [("P.LL",  "P1", (fun r -> true),
             (fun r -> { r with t1 = r.x; a1 = 0 }))]);
    ("P1", [("P.inc",   "P2", (fun r -> true),
             (fun r -> { r with t1 = r.t1 + 1 }))]);
    ("P2", [("P.SC", "P3", (fun r -> true),
             (fun r ->
               if r.a1 = 0 then
                 { r with x = r.t1; t1 = 0; a2 = 1 }
               else
                 { r with t1 = 1 }))]);
    ("P3", [("P.retry", "P0", (fun r -> r.t1 = 1),
             (fun r -> r));
            ("P.done", "P4", (fun r -> r.t1 = 0),
             (fun r -> r))]);
    ("P4", []);
  ]


let process_Q = [
    ("Q0", [("Q.LL",  "Q1", (fun r -> true),
             (fun r -> { r with t2 = r.x; a2 = 0 }))]);
    ("Q1", [("Q.inc",   "Q2", (fun r -> true),
             (fun r -> { r with t2 = r.t2 + 1 }))]);
    ("Q2", [("Q.SC", "Q3", (fun r -> true),
             (fun r ->
               if r.a2 = 0 then
                 { r with x = r.t2; t2 = 0; a1 = 1 }
               else
                 { r with t2 = 1 }))]);
    ("Q3", [("Q.retry", "Q0", (fun r -> r.t2 = 1),
             (fun r -> r));
            ("Q.done", "Q4", (fun r -> r.t2 = 0),
             (fun r -> r))]);
    ("Q4", []);
  ]

let ps = [process_P; process_Q]

let () =
  viz_process "m_llsc_P" process_P;
  viz_process "m_llsc_Q" process_Q;
  let lts = concurrent_composition r0 ps in
  lts_print_deadlocks stdout show_sv lts;
  viz_lts "m_llsc" show_sv lts