diff --git a/src/datarace/dune b/src/datarace/dune new file mode 100644 index 000000000..0618ec2c9 --- /dev/null +++ b/src/datarace/dune @@ -0,0 +1,18 @@ +;; Tests of references, mutable record fields and arrays to demonstrate read/write data-races + +;; this prevents the tests from running on a default build + +(alias + (name default) + (deps lin_tests.exe)) + +(executable + (name lin_tests) + (libraries qcheck-lin.domain)) + +(rule + (alias runtest) + (package multicoretests) + (deps lin_tests.exe) + (action + (run ./%{deps} --verbose))) diff --git a/src/datarace/lin_tests.ml b/src/datarace/lin_tests.ml new file mode 100644 index 000000000..23e0b158e --- /dev/null +++ b/src/datarace/lin_tests.ml @@ -0,0 +1,75 @@ +module Refs = struct + type t = int ref * int ref + + let set_fst (fst, _) v = fst := v + let get_fst (fst, _) = !fst + let set_snd (_, snd) v = snd := v + let get_snd (_, snd) = !snd + + let init () = ref 0, ref 0 + + let cleanup _ = () + + open Lin_base + + let api = + [ val_ "set_fst" set_fst (t @-> nat_small @-> returning unit) + ; val_ "set_snd" set_snd (t @-> nat_small @-> returning unit) + ; val_ "get_fst" get_fst (t @-> returning nat_small) + ; val_ "get_snd" get_snd (t @-> returning nat_small) + ] +end + +module Mutables = struct + type t = { mutable fst : int ; mutable snd : int } + + let set_fst t v = t.fst <- v + let set_snd t v = t.snd <- v + let get_fst t = t.fst + let get_snd t = t.snd + + let init () = { fst = 0 ; snd = 0 } + + let cleanup _ = () + + open Lin_base + + let api = + [ val_ "set_fst" set_fst (t @-> nat_small @-> returning unit) + ; val_ "set_snd" set_snd (t @-> nat_small @-> returning unit) + ; val_ "get_fst" get_fst (t @-> returning nat_small) + ; val_ "get_snd" get_snd (t @-> returning nat_small) + ] +end + +module Array = struct + type t = int array + + let len = 2 + + let init () = Array.make len 0 + + let cleanup _ = () + + open Lin_base + + let index = int_bound (len - 1) + + let api = + [ val_ "set" Array.set (t @-> index @-> nat_small @-> returning unit) + ; val_ "get" Array.get (t @-> index @-> returning nat_small) + ] +end + +module Test_refs = Lin_domain.Make(Refs) +module Test_mutable = Lin_domain.Make(Mutables) +module Test_array = Lin_domain.Make(Array) + +let count = 100_000 + +let () = + QCheck_base_runner.run_tests_main + [ Test_refs.neg_lin_test ~count ~name:"Data race: Refs" + ; Test_mutable.neg_lin_test ~count ~name:"Data race: Mutables" + ; Test_array.neg_lin_test ~count ~name:"Data race: Array" + ]