Skip to content

Instantly share code, notes, and snippets.

@hatsugai
Created December 8, 2019 00:34
Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment