From 3a9a724b7f9e73b342883b8a2e6d861a29b829ad Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 19 Dec 2024 10:52:11 +0200 Subject: [PATCH 1/5] Simplified core algorithm for verification purposes --- doc/dune | 3 ++ doc/simplified.ml | 92 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 95 insertions(+) create mode 100644 doc/simplified.ml diff --git a/doc/dune b/doc/dune index 4bfc69d7..92458f36 100644 --- a/doc/dune +++ b/doc/dune @@ -6,3 +6,6 @@ (enabled_if (>= %{ocaml_version} 5.0.0)) (files gkmz-with-read-only-cmp-ops.md scheduler-interop.md)) + +(test + (name simplified)) diff --git a/doc/simplified.ml b/doc/simplified.ml new file mode 100644 index 00000000..ea762d54 --- /dev/null +++ b/doc/simplified.ml @@ -0,0 +1,92 @@ +module Kcas : sig + type 'a loc + + val make : 'a -> 'a loc + val get : 'a loc -> 'a + + type cas = CAS : 'a loc * 'a * 'a -> cas | CMP : 'a loc * 'a -> cas + + val atomically : cas list -> bool +end = struct + type 'a loc = 'a state Atomic.t + and 'a state = { before : 'a; after : 'a; casn : casn } + and cass = CASS : 'a loc * 'a state -> cass + and casn = status Atomic.t + and status = Undetermined of cass list | After | Before + + let make after = + Atomic.make { before = after; after; casn = Atomic.make After } + + type cas = CAS : 'a loc * 'a * 'a -> cas | CMP : 'a loc * 'a -> cas + + let is_cmp casn state = state.casn != casn + + let finish casn desired = + match Atomic.get casn with + | After -> true + | Before -> false + | Undetermined cass as current -> + let desired = + if + desired == After + && cass + |> List.exists @@ fun (CASS (loc, state)) -> + is_cmp casn state && Atomic.get loc != state + then Before + else desired + in + Atomic.compare_and_set casn current desired |> ignore; + Atomic.get casn == After + + let rec gkmz casn = function + | [] -> finish casn After + | CASS (loc, desired) :: continue as retry -> begin + let current = Atomic.get loc in + if desired == current then gkmz casn continue + else if is_cmp casn desired then finish casn Before + else + let current_value = + if is_after current.casn then current.after else current.before + in + if current_value != desired.before then finish casn Before + else + match Atomic.get casn with + | Undetermined _ -> + if Atomic.compare_and_set loc current desired then + gkmz casn continue + else gkmz casn retry + | After -> true + | Before -> false + end + + and is_after casn = + match Atomic.get casn with + | Undetermined cass -> gkmz casn cass + | After -> true + | Before -> false + + let get loc = + let state = Atomic.get loc in + if is_after state.casn then state.after else state.before + + let atomically logical_cas_list = + let casn = Atomic.make After in + let cass = + logical_cas_list + |> List.map @@ function + | CAS (loc, before, after) -> CASS (loc, { before; after; casn }) + | CMP (loc, expected) -> + let current = Atomic.get loc in + if get loc != expected || Atomic.get loc != current then raise Exit + else CASS (loc, current) + in + Atomic.set casn (Undetermined cass); + gkmz casn cass + + let atomically logical_cas_list = + try atomically logical_cas_list with Exit -> false + + let get loc = + let state = Atomic.get loc in + if is_after state.casn then state.after else state.before +end From f604aa15608401cdb769dbed769ff5c49e275f1b Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 19 Dec 2024 12:25:47 +0200 Subject: [PATCH 2/5] Use separate CAS and CMP lists --- doc/simplified.ml | 61 ++++++++++++++++++++++++----------------------- 1 file changed, 31 insertions(+), 30 deletions(-) diff --git a/doc/simplified.ml b/doc/simplified.ml index ea762d54..70f6ae54 100644 --- a/doc/simplified.ml +++ b/doc/simplified.ml @@ -4,34 +4,38 @@ module Kcas : sig val make : 'a -> 'a loc val get : 'a loc -> 'a - type cas = CAS : 'a loc * 'a * 'a -> cas | CMP : 'a loc * 'a -> cas + type cas = CAS : 'a loc * 'a * 'a -> cas + type cmp = CMP : 'a loc * 'a -> cmp - val atomically : cas list -> bool + val atomically : cas list -> cmp list -> bool end = struct type 'a loc = 'a state Atomic.t and 'a state = { before : 'a; after : 'a; casn : casn } and cass = CASS : 'a loc * 'a state -> cass and casn = status Atomic.t - and status = Undetermined of cass list | After | Before + + and status = + | Undetermined of { cass : cass list; cmps : cass list } + | After + | Before let make after = Atomic.make { before = after; after; casn = Atomic.make After } - type cas = CAS : 'a loc * 'a * 'a -> cas | CMP : 'a loc * 'a -> cas - - let is_cmp casn state = state.casn != casn + type cas = CAS : 'a loc * 'a * 'a -> cas + type cmp = CMP : 'a loc * 'a -> cmp let finish casn desired = match Atomic.get casn with | After -> true | Before -> false - | Undetermined cass as current -> + | Undetermined { cmps; _ } as current -> let desired = if desired == After - && cass + && cmps |> List.exists @@ fun (CASS (loc, state)) -> - is_cmp casn state && Atomic.get loc != state + Atomic.get loc != state then Before else desired in @@ -43,11 +47,8 @@ end = struct | CASS (loc, desired) :: continue as retry -> begin let current = Atomic.get loc in if desired == current then gkmz casn continue - else if is_cmp casn desired then finish casn Before else - let current_value = - if is_after current.casn then current.after else current.before - in + let current_value = get_from current in if current_value != desired.before then finish casn Before else match Atomic.get casn with @@ -59,34 +60,34 @@ end = struct | Before -> false end - and is_after casn = - match Atomic.get casn with - | Undetermined cass -> gkmz casn cass - | After -> true - | Before -> false - - let get loc = - let state = Atomic.get loc in - if is_after state.casn then state.after else state.before + and get_from : 'a. 'a state -> 'a = + fun state -> + match Atomic.get state.casn with + | Undetermined { cass; _ } -> + if gkmz state.casn cass then state.after else state.before + | After -> state.after + | Before -> state.before - let atomically logical_cas_list = + let atomically logical_cas_list logical_cmp_list = let casn = Atomic.make After in let cass = logical_cas_list |> List.map @@ function | CAS (loc, before, after) -> CASS (loc, { before; after; casn }) + in + let cmps = + logical_cmp_list + |> List.map @@ function | CMP (loc, expected) -> let current = Atomic.get loc in - if get loc != expected || Atomic.get loc != current then raise Exit + if get_from current != expected then raise Exit else CASS (loc, current) in - Atomic.set casn (Undetermined cass); + Atomic.set casn (Undetermined { cass; cmps }); gkmz casn cass - let atomically logical_cas_list = - try atomically logical_cas_list with Exit -> false + let atomically logical_cas_list logical_cmp_list = + try atomically logical_cas_list logical_cmp_list with Exit -> false - let get loc = - let state = Atomic.get loc in - if is_after state.casn then state.after else state.before + let get loc = get_from (Atomic.get loc) end From b2ca51911f572f981782d2fca409f2c92238667e Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 19 Dec 2024 12:30:15 +0200 Subject: [PATCH 3/5] Smoke --- doc/simplified.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/simplified.ml b/doc/simplified.ml index 70f6ae54..d21e96e2 100644 --- a/doc/simplified.ml +++ b/doc/simplified.ml @@ -91,3 +91,10 @@ end = struct let get loc = get_from (Atomic.get loc) end + +let () = + let x = Kcas.make 82 in + let y = Kcas.make 40 in + assert (Kcas.atomically [ CAS (x, 82, 42) ] [ CMP (y, 40) ]); + assert (Kcas.get x == 42 && Kcas.get y == 40); + () From 4a5d840cbc2404ff13ae5c094bc97293bda286b5 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 19 Dec 2024 15:12:13 +0200 Subject: [PATCH 4/5] Add awaiters and cleanup --- doc/simplified.ml | 89 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 68 insertions(+), 21 deletions(-) diff --git a/doc/simplified.ml b/doc/simplified.ml index d21e96e2..2a4abf4c 100644 --- a/doc/simplified.ml +++ b/doc/simplified.ml @@ -1,4 +1,12 @@ -module Kcas : sig +module type Awaiter = sig + type t + + val signal : t -> unit +end + +module Make (Awaiter : Awaiter) : sig + module Awaiter : Awaiter + type 'a loc val make : 'a -> 'a loc @@ -9,18 +17,36 @@ module Kcas : sig val atomically : cas list -> cmp list -> bool end = struct + module Awaiter = Awaiter + type 'a loc = 'a state Atomic.t - and 'a state = { before : 'a; after : 'a; casn : casn } - and cass = CASS : 'a loc * 'a state -> cass + + and 'a state = { + mutable before : 'a; + mutable after : 'a; + casn : casn; + awaiters : Awaiter.t list; + } + + and cass = + | CASS : { + loc : 'a loc; + desired : 'a state; + mutable awaiters : Awaiter.t list; + } + -> cass + + and cmps = CMPS : { loc : 'a loc; current : 'a state } -> cmps and casn = status Atomic.t and status = - | Undetermined of { cass : cass list; cmps : cass list } + | Undetermined of { cass : cass list; cmps : cmps list } | After | Before let make after = - Atomic.make { before = after; after; casn = Atomic.make After } + Atomic.make + { before = after; after; casn = Atomic.make After; awaiters = [] } type cas = CAS : 'a loc * 'a * 'a -> cas type cmp = CMP : 'a loc * 'a -> cmp @@ -29,31 +55,44 @@ end = struct match Atomic.get casn with | After -> true | Before -> false - | Undetermined { cmps; _ } as current -> + | Undetermined undetermined as current -> let desired = if desired == After - && cmps - |> List.exists @@ fun (CASS (loc, state)) -> - Atomic.get loc != state + && undetermined.cmps + |> List.exists @@ fun (CMPS cmps) -> + Atomic.get cmps.loc != cmps.current then Before else desired in - Atomic.compare_and_set casn current desired |> ignore; + if Atomic.compare_and_set casn current desired then begin + if desired == After then begin + undetermined.cass + |> List.iter @@ fun (CASS cass) -> + List.iter Awaiter.signal cass.awaiters; + cass.desired.before <- cass.desired.after + end + else begin + undetermined.cass + |> List.iter @@ fun (CASS cass) -> + cass.desired.after <- cass.desired.before + end + end; Atomic.get casn == After let rec gkmz casn = function | [] -> finish casn After - | CASS (loc, desired) :: continue as retry -> begin - let current = Atomic.get loc in - if desired == current then gkmz casn continue + | CASS cass :: continue as retry -> begin + let current = Atomic.get cass.loc in + if cass.desired == current then gkmz casn continue else let current_value = get_from current in - if current_value != desired.before then finish casn Before + if current_value != cass.desired.before then finish casn Before else match Atomic.get casn with | Undetermined _ -> - if Atomic.compare_and_set loc current desired then + cass.awaiters <- current.awaiters; + if Atomic.compare_and_set cass.loc current cass.desired then gkmz casn continue else gkmz casn retry | After -> true @@ -73,7 +112,9 @@ end = struct let cass = logical_cas_list |> List.map @@ function - | CAS (loc, before, after) -> CASS (loc, { before; after; casn }) + | CAS (loc, before, after) -> + let next = { before; after; casn; awaiters = [] } in + CASS { loc; desired = next; awaiters = [] } in let cmps = logical_cmp_list @@ -81,7 +122,7 @@ end = struct | CMP (loc, expected) -> let current = Atomic.get loc in if get_from current != expected then raise Exit - else CASS (loc, current) + else CMPS { loc; current } in Atomic.set casn (Undetermined { cass; cmps }); gkmz casn cass @@ -93,8 +134,14 @@ end = struct end let () = - let x = Kcas.make 82 in - let y = Kcas.make 40 in - assert (Kcas.atomically [ CAS (x, 82, 42) ] [ CMP (y, 40) ]); - assert (Kcas.get x == 42 && Kcas.get y == 40); + let module Awaiter = struct + type t = unit + + let signal = ignore + end in + let module STM = Make (Awaiter) in + let x = STM.make 82 in + let y = STM.make 40 in + assert (STM.atomically [ CAS (x, 82, 42) ] [ CMP (y, 40) ]); + assert (STM.get x == 42 && STM.get y == 40); () From 342843b7f571967f780a648ec1d68f54f3087f9b Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Fri, 20 Dec 2024 11:27:13 +0200 Subject: [PATCH 5/5] Dependencies --- doc/dune | 8 ++++++-- dune-project | 4 ++++ kcas.opam | 1 + 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/doc/dune b/doc/dune index 92458f36..238efb2a 100644 --- a/doc/dune +++ b/doc/dune @@ -4,8 +4,12 @@ (package kcas) (package kcas_data)) (enabled_if - (>= %{ocaml_version} 5.0.0)) + (<= 5.0.0 %{ocaml_version})) (files gkmz-with-read-only-cmp-ops.md scheduler-interop.md)) (test - (name simplified)) + (package kcas) + (name simplified) + (build_if + (<= 5.0.0 %{ocaml_version})) + (libraries alcotest dscheck)) diff --git a/dune-project b/dune-project index b7572267..9bd9b541 100644 --- a/dune-project +++ b/dune-project @@ -48,6 +48,10 @@ (and (>= 1.8.0) :with-test)) + (dscheck + (and + (>= 0.5.0) + :with-test)) (qcheck-core (and (>= 0.21.2) diff --git a/kcas.opam b/kcas.opam index acfd08ad..4eb9ec83 100644 --- a/kcas.opam +++ b/kcas.opam @@ -24,6 +24,7 @@ depends: [ "multicore-magic" {>= "2.3.0"} "domain_shims" {>= "0.1.0" & with-test} "alcotest" {>= "1.8.0" & with-test} + "dscheck" {>= "0.5.0" & with-test} "qcheck-core" {>= "0.21.2" & with-test} "qcheck-stm" {>= "0.3" & with-test} "mdx" {>= "2.4.1" & with-test}