From 0e12763b2355f882bca84045f20f07a1c69918c9 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 7 Dec 2023 17:06:00 +0100 Subject: [PATCH 1/3] Adjust Semaphore.Counting test to include a run without racy get_value --- src/semaphore/stm_tests.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/semaphore/stm_tests.ml b/src/semaphore/stm_tests.ml index c00a0acfd..efee0356e 100644 --- a/src/semaphore/stm_tests.ml +++ b/src/semaphore/stm_tests.ml @@ -73,11 +73,19 @@ module SCConf = end module SCTest_seq = STM_sequential.Make(SCConf) -module SCTest_dom = STM_domain.Make(SCConf) +module SCTest_dom_gv = STM_domain.Make(SCConf) +module SCTest_dom = STM_domain.Make(struct + include SCConf + let arb_cmd s = + let cmds = [ Release; TryAcquire; ] in (* No GetValue *) + let cmds = if s > 0 then Acquire :: cmds else cmds in + QCheck.make ~print:show_cmd (Gen.oneofl cmds) + end) let _ = QCheck_base_runner.run_tests_main (let count = 200 in - [SCTest_seq.agree_test ~count ~name:"STM Semaphore.Counting test sequential"; - SCTest_dom.agree_test_par ~count ~name:"STM Semaphore.Counting test parallel"; + [SCTest_seq.agree_test ~count ~name:"STM Semaphore.Counting test sequential"; + SCTest_dom_gv.agree_test_par ~count ~name:"STM Semaphore.Counting test parallel (w/ get_value)"; + SCTest_dom.agree_test_par ~count ~name:"STM Semaphore.Counting test parallel (w/o get_value)"; ]) From 0824226639511825c357c0a8eee520a70007bc3e Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 7 Dec 2023 17:17:32 +0100 Subject: [PATCH 2/3] Add tests of Semaphore.Binary --- src/semaphore/dune | 8 ++++ src/semaphore/stm_tests_binary.ml | 74 +++++++++++++++++++++++++++++++ 2 files changed, 82 insertions(+) create mode 100644 src/semaphore/stm_tests_binary.ml diff --git a/src/semaphore/dune b/src/semaphore/dune index 384c9f633..8940bfe9b 100644 --- a/src/semaphore/dune +++ b/src/semaphore/dune @@ -7,3 +7,11 @@ (libraries qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose)) ) + +(test + (name stm_tests_binary) + (modules stm_tests_binary) + (package multicoretests) + (libraries qcheck-stm.sequential qcheck-stm.domain) + (action (run %{test} --verbose)) +) diff --git a/src/semaphore/stm_tests_binary.ml b/src/semaphore/stm_tests_binary.ml new file mode 100644 index 000000000..a4a45e499 --- /dev/null +++ b/src/semaphore/stm_tests_binary.ml @@ -0,0 +1,74 @@ +open QCheck +open STM + +(** parallel STM tests of Semaphore.Binary *) + +(* Semaphore API these tests will exercise + + val make : bool -> t + val release : t -> unit + val acquire : t -> unit + val try_acquire : t -> bool + +*) + +module SBConf = + struct + type sut = Semaphore.Binary.t + type state = int + + type cmd = + | Release + | Acquire + | TryAcquire + + let pp_cmd _ fmt x = + let open Util.Pp in + match x with + | Release -> cst0 "Release" fmt + | Acquire -> cst0 "Acquire" fmt + | TryAcquire -> cst0 "TryAcquire" fmt + + let show_cmd = Util.Pp.to_show pp_cmd + + let init_state = 1 + let init_sut () = Semaphore.Binary.make true + let cleanup _ = () + + let arb_cmd s = + let cmds = [ Release; TryAcquire; ] in + let cmds = if s = 1 then Acquire :: cmds else cmds in + QCheck.make ~print:show_cmd (Gen.oneofl cmds) + + let next_state c s = match c with + | Release -> 1 + | Acquire -> 0 + | TryAcquire -> if s = 1 then 0 else 0 + + let run c sem = + match c with + | Release -> Res (unit, Semaphore.Binary.release sem) + | Acquire -> Res (unit, Semaphore.Binary.acquire sem) + | TryAcquire -> Res (bool, Semaphore.Binary.try_acquire sem) + + let precond c s = + match c with + | Acquire -> s = 1 + | _ -> true + let postcond c s res = + match c,res with + | Release, Res ((Unit,_), _) + | Acquire, Res ((Unit,_), _) -> true + | TryAcquire, Res ((Bool,_),r) -> r = (s = 1) + | _ -> false + end + +module SBTest_seq = STM_sequential.Make(SBConf) +module SBTest_dom = STM_domain.Make(SBConf) + +let _ = + QCheck_base_runner.run_tests_main + (let count = 500 in + [SBTest_seq.agree_test ~count ~name:"STM Semaphore.Binary test sequential"; + SBTest_dom.agree_test_par ~count ~name:"STM Semaphore.Binary test parallel"; + ]) From 1311e743b7fbe4f1c0be1ca151eb5e3a6150d007 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 7 Dec 2023 17:22:05 +0100 Subject: [PATCH 3/3] Rename src/semaphore/stm_tests.ml accordingly --- src/semaphore/dune | 6 +++--- src/semaphore/{stm_tests.ml => stm_tests_counting.ml} | 0 2 files changed, 3 insertions(+), 3 deletions(-) rename src/semaphore/{stm_tests.ml => stm_tests_counting.ml} (100%) diff --git a/src/semaphore/dune b/src/semaphore/dune index 8940bfe9b..a714e8be5 100644 --- a/src/semaphore/dune +++ b/src/semaphore/dune @@ -1,13 +1,13 @@ ;; Tests of Semaphore.Counting - (test - (name stm_tests) - (modules stm_tests) + (name stm_tests_counting) + (modules stm_tests_counting) (package multicoretests) (libraries qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose)) ) +;; Tests of Semaphore.Binary (test (name stm_tests_binary) (modules stm_tests_binary) diff --git a/src/semaphore/stm_tests.ml b/src/semaphore/stm_tests_counting.ml similarity index 100% rename from src/semaphore/stm_tests.ml rename to src/semaphore/stm_tests_counting.ml