From 082fc44faf9edbd02db85fd63706977a8b480d08 Mon Sep 17 00:00:00 2001 From: Kaustubh Maske Patil <37668193+nikochiko@users.noreply.github.com> Date: Wed, 1 Mar 2023 14:54:37 +0530 Subject: [PATCH 01/22] Add a simple example of Michael_scott_queue --- examples/dune | 3 +++ examples/michael_scott_queue.ml | 20 ++++++++++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 examples/dune create mode 100644 examples/michael_scott_queue.ml diff --git a/examples/dune b/examples/dune new file mode 100644 index 00000000..f7fe0bbb --- /dev/null +++ b/examples/dune @@ -0,0 +1,3 @@ +(executables + (names michael_scott_queue) + (libraries lockfree)) diff --git a/examples/michael_scott_queue.ml b/examples/michael_scott_queue.ml new file mode 100644 index 00000000..74dbafe3 --- /dev/null +++ b/examples/michael_scott_queue.ml @@ -0,0 +1,20 @@ +open Lockfree.Michael_scott_queue + +let push_work_pop queue item = + push queue item; + for _ = 1 to 100_000_000 do + (* do other work *) + ignore () + done; + match pop queue with + | Some v -> Printf.printf "pushed %d and popped %d\n" item v + | None -> failwith "pop failed: empty list" + +let main () = + let ms_q = create () in + let d1 = Domain.spawn(fun _ -> push_work_pop ms_q 1) in + let d2 = Domain.spawn(fun _ -> push_work_pop ms_q 2) in + let d3 = Domain.spawn(fun _ -> push_work_pop ms_q 3) in + Domain.join d1; Domain.join d2; Domain.join d3 + +let _ = main () From f07b56b59c78113bfc09ac989ef4c7d1a3d7067a Mon Sep 17 00:00:00 2001 From: Kaustubh Maske Patil <37668193+nikochiko@users.noreply.github.com> Date: Thu, 2 Mar 2023 03:28:55 +0530 Subject: [PATCH 02/22] Add a wider range of examples --- examples/michael_scott_queue.ml | 90 ++++++++++++++++++++++++++++----- 1 file changed, 76 insertions(+), 14 deletions(-) diff --git a/examples/michael_scott_queue.ml b/examples/michael_scott_queue.ml index 74dbafe3..87db8828 100644 --- a/examples/michael_scott_queue.ml +++ b/examples/michael_scott_queue.ml @@ -1,20 +1,82 @@ open Lockfree.Michael_scott_queue -let push_work_pop queue item = - push queue item; - for _ = 1 to 100_000_000 do - (* do other work *) - ignore () - done; - match pop queue with - | Some v -> Printf.printf "pushed %d and popped %d\n" item v - | None -> failwith "pop failed: empty list" +let n_domains = 4 + +let single_push_and_pop () = + let ms_q = create () in + let item = 1 in + push ms_q item; + Printf.printf "single_push_and_pop: pushed %d\n" item; + match pop ms_q with + | None -> failwith "single_push_and_pop: queue is empty" + | Some v -> Printf.printf "single_push_and_pop: popped %d\n" v + +let concurrent_push () = + let ms_q = create () in + let item = 42 in + + (* push concurrently *) + let pusher _ = + push ms_q item; + Printf.printf "concurrent_push: pushed %d\n" item + in + let domains = Array.init n_domains (fun _ -> Domain.spawn pusher) in + Array.iter Domain.join domains; + + (* pop sequentially and examine *) + for _ = 1 to n_domains do + match pop ms_q with + | None -> failwith "concurrent_push: queue is empty" + | Some v -> Printf.printf "concurrent_push: popped %d\n" v + done + +let concurrent_pop () = + let ms_q = create () in + let item = 42 in + + (* push sequentially *) + for _ = 1 to n_domains do + push ms_q item; + Printf.printf "concurrent_pop: pushed %d\n" item + done; + + (* pop concurrently *) + let popper _ = + match pop ms_q with + | None -> failwith "concurrent_pop: list is empty" + | Some v -> Printf.printf "concurrent_pop: popped %d\n" v + in + let domains = Array.init n_domains (fun _ -> Domain.spawn popper) in + Array.iter Domain.join domains + +let concurrent_push_and_pop () = + let ms_q = create () in + let item = 42 in + + (* push and pop, both concurrently *) + let pusher _ = + push ms_q item; + Printf.printf "concurrent_push_and_pop: pushed %d\n" item + in + let rec pop_one _ = + match pop ms_q with + | None -> pop_one () (* keep trying until an item is popped *) + | Some v -> Printf.printf "concurrent_push_and_pop: popped %d\n" v + in + + (* n_domains/2 pushers, n_domains/2 poppers concurrently *) + let popper_domains = + Array.init (n_domains / 2) (fun _ -> Domain.spawn pop_one) + in + let pusher_domains = + Array.init (n_domains / 2) (fun _ -> Domain.spawn pusher) + in + Array.iter Domain.join (Array.append pusher_domains popper_domains) let main () = - let ms_q = create () in - let d1 = Domain.spawn(fun _ -> push_work_pop ms_q 1) in - let d2 = Domain.spawn(fun _ -> push_work_pop ms_q 2) in - let d3 = Domain.spawn(fun _ -> push_work_pop ms_q 3) in - Domain.join d1; Domain.join d2; Domain.join d3 + single_push_and_pop (); + concurrent_push (); + concurrent_pop (); + concurrent_push_and_pop () let _ = main () From e1488576737e19f0ffeff830c18c82a8ec2c7554 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Fri, 10 Mar 2023 10:17:01 +0200 Subject: [PATCH 03/22] Fix space leaks of Michael-Scott queue Fixes issue #63 --- src/michael_scott_queue.ml | 81 ++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 43 deletions(-) diff --git a/src/michael_scott_queue.ml b/src/michael_scott_queue.ml index 055c0d98..24a30b6d 100644 --- a/src/michael_scott_queue.ml +++ b/src/michael_scott_queue.ml @@ -1,6 +1,7 @@ (* * Copyright (c) 2015, Théo Laurent * Copyright (c) 2015, KC Sivaramakrishnan + * Copyright (c) 2023, Vesa Karvonen * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above @@ -18,65 +19,63 @@ (* Michael-Scott queue *) type 'a node = Nil | Next of 'a * 'a node Atomic.t -type 'a t = { head : 'a node Atomic.t; tail : 'a node Atomic.t } + +type 'a t = { + head : 'a node Atomic.t Atomic.t; + tail : 'a node Atomic.t Atomic.t; +} let create () = - let head = Next (Obj.magic (), Atomic.make Nil) in - { head = Atomic.make head; tail = Atomic.make head } + let next = Atomic.make Nil in + { head = Atomic.make next; tail = Atomic.make next } -let is_empty q = - match Atomic.get q.head with - | Nil -> failwith "MSQueue.is_empty: impossible" - | Next (_, x) -> ( match Atomic.get x with Nil -> true | _ -> false) +let is_empty { head; _ } = Atomic.get (Atomic.get head) == Nil -let pop q = +let pop { head; _ } = let b = Backoff.create () in let rec loop () = - let s = Atomic.get q.head in - let nhead = - match s with - | Nil -> failwith "MSQueue.pop: impossible" - | Next (_, x) -> Atomic.get x - in - match nhead with + let old_head = Atomic.get head in + match Atomic.get old_head with | Nil -> None - | Next (v, _) when Atomic.compare_and_set q.head s nhead -> Some v + | Next (value, next) when Atomic.compare_and_set head old_head next -> + Some value | _ -> Backoff.once b; loop () in loop () -let push q v = +let rec fix_tail tail old_tail new_tail = + if Atomic.compare_and_set tail old_tail new_tail then + match Atomic.get new_tail with + | Nil -> () + | Next (_, new_new_tail) -> fix_tail tail new_tail new_new_tail + +let push { tail; _ } value = let rec find_tail_and_enq curr_end node = - if Atomic.compare_and_set curr_end Nil node then () - else + if not (Atomic.compare_and_set curr_end Nil node) then match Atomic.get curr_end with | Nil -> find_tail_and_enq curr_end node | Next (_, n) -> find_tail_and_enq n node in - let newnode = Next (v, Atomic.make Nil) in - let tail = Atomic.get q.tail in - match tail with - | Nil -> failwith "HW_MSQueue.push: impossible" - | Next (_, n) -> - find_tail_and_enq n newnode; - ignore (Atomic.compare_and_set q.tail tail newnode) + let new_tail = Atomic.make Nil in + let newnode = Next (value, new_tail) in + let old_tail = Atomic.get tail in + find_tail_and_enq old_tail newnode; + if Atomic.compare_and_set tail old_tail new_tail then + match Atomic.get new_tail with + | Nil -> () + | Next (_, new_new_tail) -> fix_tail tail new_tail new_new_tail -let clean_until q f = +let clean_until { head; _ } f = let b = Backoff.create () in let rec loop () = - let s = Atomic.get q.head in - let nhead = - match s with - | Nil -> failwith "MSQueue.pop: impossible" - | Next (_, x) -> Atomic.get x - in - match nhead with + let old_head = Atomic.get head in + match Atomic.get old_head with | Nil -> () - | Next (v, _) -> - if not (f v) then - if Atomic.compare_and_set q.head s nhead then ( + | Next (value, next) -> + if not (f value) then + if Atomic.compare_and_set head old_head next then ( Backoff.reset b; loop ()) else ( @@ -88,9 +87,5 @@ let clean_until q f = type 'a cursor = 'a node -let snapshot q = - match Atomic.get q.head with - | Nil -> failwith "MSQueue.snapshot: impossible" - | Next (_, n) -> Atomic.get n - -let next c = match c with Nil -> None | Next (a, n) -> Some (a, Atomic.get n) +let snapshot { head; _ } = Atomic.get (Atomic.get head) +let next = function Nil -> None | Next (a, n) -> Some (a, Atomic.get n) From cf89702a70187d662cb06734f3152115c6bd142b Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 16 Mar 2023 08:58:04 +0200 Subject: [PATCH 04/22] Run on 5.0.0 rather than 5.0.0~alpha0 --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 190cf6f0..8853c32a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -15,7 +15,7 @@ jobs: - ubuntu-latest - macos-latest ocaml-compiler: - - ocaml-base-compiler.5.0.0~alpha0 + - ocaml-base-compiler.5.0.0 - ocaml-variants.5.1.0+trunk runs-on: ${{ matrix.os }} @@ -45,4 +45,4 @@ jobs: - run: opam exec -- dune build - - run: opam exec -- dune runtest \ No newline at end of file + - run: opam exec -- dune runtest From bd9b0b59e37fb3857b3109c78b67b04944d369d2 Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Mon, 20 Mar 2023 17:45:17 +0200 Subject: [PATCH 05/22] Fix the lock-free update of Michael-Scott style queue tail I realized my previous attempt suffered from pretty much the same race condition as the earlier implementations. The logic of the new tail update algorithm is as follows: > The tail update is only responsible for updating the tail as long as the new > node added still has the true tail. At any point some newly added node has the > true tail, so this responsibility ensures that the tail gets updated. To check > whether we are still responsible, we compare: `get new_tail == Nil`. If that > is false, then someone else is responsible and we can stop. The current > old_tail must be read before that check. If the `compare_and_set` fails, we > must retry. Otherwise we can stop as we've done our part. --- src/michael_scott_queue.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/michael_scott_queue.ml b/src/michael_scott_queue.ml index 24a30b6d..867153ce 100644 --- a/src/michael_scott_queue.ml +++ b/src/michael_scott_queue.ml @@ -45,11 +45,12 @@ let pop { head; _ } = in loop () -let rec fix_tail tail old_tail new_tail = - if Atomic.compare_and_set tail old_tail new_tail then - match Atomic.get new_tail with - | Nil -> () - | Next (_, new_new_tail) -> fix_tail tail new_tail new_new_tail +let rec fix_tail tail new_tail = + let old_tail = Atomic.get tail in + if + Atomic.get new_tail == Nil + && not (Atomic.compare_and_set tail old_tail new_tail) + then fix_tail tail new_tail let push { tail; _ } value = let rec find_tail_and_enq curr_end node = @@ -62,10 +63,8 @@ let push { tail; _ } value = let newnode = Next (value, new_tail) in let old_tail = Atomic.get tail in find_tail_and_enq old_tail newnode; - if Atomic.compare_and_set tail old_tail new_tail then - match Atomic.get new_tail with - | Nil -> () - | Next (_, new_new_tail) -> fix_tail tail new_tail new_new_tail + if not (Atomic.compare_and_set tail old_tail new_tail) then + fix_tail tail new_tail let clean_until { head; _ } f = let b = Backoff.create () in From 31d51fda3292522e1898aadc0f518efd441d713b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 23 Mar 2023 13:36:00 +0100 Subject: [PATCH 06/22] set QCHECK_MSG_INTERVAL to avoid clutter in CI logs --- .github/workflows/main.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8853c32a..3192d0a1 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -20,6 +20,9 @@ jobs: runs-on: ${{ matrix.os }} + env: + QCHECK_MSG_INTERVAL: '60' + steps: - name: Checkout code uses: actions/checkout@v2 From 7c5bd51399f4d499208c2b9992f42708993347b6 Mon Sep 17 00:00:00 2001 From: Louis Date: Mon, 3 Apr 2023 12:14:03 +0800 Subject: [PATCH 07/22] mark alcotest as a test dependency --- lockfree.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lockfree.opam b/lockfree.opam index 606c8818..0784d4d8 100644 --- a/lockfree.opam +++ b/lockfree.opam @@ -15,7 +15,7 @@ depends: [ "qcheck" {with-test & >= "0.18.1"} "qcheck-stm" {with-test & >= "0.1"} "qcheck-alcotest" {with-test & >= "0.18.1"} - "alcotest" {>= "1.6.0"} + "alcotest" {with-test & >= "1.6.0"} "yojson" {>= "2.0.2"} "dscheck" {with-test & >= "0.0.1"} ] From 42bd0012a049d9ce8c50c887ff53717fee00303c Mon Sep 17 00:00:00 2001 From: Kaustubh Maske Patil <37668193+nikochiko@users.noreply.github.com> Date: Sat, 8 Apr 2023 13:19:28 +0530 Subject: [PATCH 08/22] Better prints, concurrency with do_work function Add better print statements, accompanied by a pusher/popper id. Add a do_work function that calls Domain.cpu_relax a random large number of times. This makes concurrency apparent after the example is run. --- examples/michael_scott_queue.ml | 53 ++++++++++++++++----------------- 1 file changed, 26 insertions(+), 27 deletions(-) diff --git a/examples/michael_scott_queue.ml b/examples/michael_scott_queue.ml index 87db8828..69e59b6c 100644 --- a/examples/michael_scott_queue.ml +++ b/examples/michael_scott_queue.ml @@ -11,65 +11,64 @@ let single_push_and_pop () = | None -> failwith "single_push_and_pop: queue is empty" | Some v -> Printf.printf "single_push_and_pop: popped %d\n" v +let do_work () = + (* do some work *) + for _ = 1 to Random.int 100_000 do + Domain.cpu_relax () + done + let concurrent_push () = let ms_q = create () in - let item = 42 in (* push concurrently *) - let pusher _ = + let pusher id item _ = + do_work (); push ms_q item; - Printf.printf "concurrent_push: pushed %d\n" item + Printf.printf "concurrent_push: pushed %d (pusher id: %d)\n" item id in - let domains = Array.init n_domains (fun _ -> Domain.spawn pusher) in - Array.iter Domain.join domains; - - (* pop sequentially and examine *) - for _ = 1 to n_domains do - match pop ms_q with - | None -> failwith "concurrent_push: queue is empty" - | Some v -> Printf.printf "concurrent_push: popped %d\n" v - done + let domains = Array.init n_domains (fun i -> Domain.spawn (pusher i (i+1))) in + Array.iter Domain.join domains let concurrent_pop () = let ms_q = create () in - let item = 42 in (* push sequentially *) - for _ = 1 to n_domains do - push ms_q item; - Printf.printf "concurrent_pop: pushed %d\n" item + for i = 1 to n_domains do + push ms_q i done; (* pop concurrently *) - let popper _ = + let popper id _ = + do_work (); match pop ms_q with | None -> failwith "concurrent_pop: list is empty" - | Some v -> Printf.printf "concurrent_pop: popped %d\n" v + | Some v -> Printf.printf "concurrent_pop: popped %d (popper id: %d)\n" v id in - let domains = Array.init n_domains (fun _ -> Domain.spawn popper) in + let domains = Array.init n_domains (fun i -> Domain.spawn (popper i)) in Array.iter Domain.join domains let concurrent_push_and_pop () = let ms_q = create () in - let item = 42 in (* push and pop, both concurrently *) - let pusher _ = + let pusher id item _ = + do_work (); push ms_q item; - Printf.printf "concurrent_push_and_pop: pushed %d\n" item + Printf.printf "concurrent_push_and_pop: pushed %d (pusher id: %d)\n" item id in - let rec pop_one _ = + let rec pop_one id _ = + do_work (); match pop ms_q with - | None -> pop_one () (* keep trying until an item is popped *) - | Some v -> Printf.printf "concurrent_push_and_pop: popped %d\n" v + | None -> pop_one id () (* keep trying until an item is popped *) + | Some v -> Printf.printf "concurrent_push_and_pop: popped %d (popper id: %d)\n" v id in (* n_domains/2 pushers, n_domains/2 poppers concurrently *) let popper_domains = - Array.init (n_domains / 2) (fun _ -> Domain.spawn pop_one) + Array.init (n_domains / 2) (fun i -> Domain.spawn (pop_one i)) in let pusher_domains = - Array.init (n_domains / 2) (fun _ -> Domain.spawn pusher) + Array.init (n_domains / 2) (fun i -> Domain.spawn (pusher i (i+1))) in Array.iter Domain.join (Array.append pusher_domains popper_domains) From 970cd86ce336734dfa5e85710c9c8c3cc474adfa Mon Sep 17 00:00:00 2001 From: Kaustubh Maske Patil <37668193+nikochiko@users.noreply.github.com> Date: Thu, 11 May 2023 03:49:08 +0530 Subject: [PATCH 09/22] Add Random.self_init and run dune fmt --- examples/michael_scott_queue.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/examples/michael_scott_queue.ml b/examples/michael_scott_queue.ml index 69e59b6c..8c4060b9 100644 --- a/examples/michael_scott_queue.ml +++ b/examples/michael_scott_queue.ml @@ -12,10 +12,10 @@ let single_push_and_pop () = | Some v -> Printf.printf "single_push_and_pop: popped %d\n" v let do_work () = - (* do some work *) - for _ = 1 to Random.int 100_000 do - Domain.cpu_relax () - done + (* do some work *) + for _ = 1 to Random.int 100_000 do + Domain.cpu_relax () + done let concurrent_push () = let ms_q = create () in @@ -26,7 +26,9 @@ let concurrent_push () = push ms_q item; Printf.printf "concurrent_push: pushed %d (pusher id: %d)\n" item id in - let domains = Array.init n_domains (fun i -> Domain.spawn (pusher i (i+1))) in + let domains = + Array.init n_domains (fun i -> Domain.spawn (pusher i (i + 1))) + in Array.iter Domain.join domains let concurrent_pop () = @@ -42,7 +44,7 @@ let concurrent_pop () = do_work (); match pop ms_q with | None -> failwith "concurrent_pop: list is empty" - | Some v -> Printf.printf "concurrent_pop: popped %d (popper id: %d)\n" v id + | Some v -> Printf.printf "concurrent_pop: popped %d (popper id: %d)\n" v id in let domains = Array.init n_domains (fun i -> Domain.spawn (popper i)) in Array.iter Domain.join domains @@ -60,7 +62,9 @@ let concurrent_push_and_pop () = do_work (); match pop ms_q with | None -> pop_one id () (* keep trying until an item is popped *) - | Some v -> Printf.printf "concurrent_push_and_pop: popped %d (popper id: %d)\n" v id + | Some v -> + Printf.printf "concurrent_push_and_pop: popped %d (popper id: %d)\n" v + id in (* n_domains/2 pushers, n_domains/2 poppers concurrently *) @@ -68,11 +72,12 @@ let concurrent_push_and_pop () = Array.init (n_domains / 2) (fun i -> Domain.spawn (pop_one i)) in let pusher_domains = - Array.init (n_domains / 2) (fun i -> Domain.spawn (pusher i (i+1))) + Array.init (n_domains / 2) (fun i -> Domain.spawn (pusher i (i + 1))) in Array.iter Domain.join (Array.append pusher_domains popper_domains) let main () = + Random.self_init (); single_push_and_pop (); concurrent_push (); concurrent_pop (); From ef6414f280cf1e27c33aeb155c3cf0038978081d Mon Sep 17 00:00:00 2001 From: Sudha Parimala Date: Thu, 11 May 2023 10:32:59 +0530 Subject: [PATCH 10/22] Adopt OCaml Code of Conduct This code of conduct lives in [ocaml/code-of-conduct](https://github.com/ocaml/code-of-conduct) and has been discussed in [this thread](https://discuss.ocaml.org/t/ocaml-community-code-of-conduct/10494). It has been adopted by the OCaml compiler and many platform tools. After a discussion we propose adopting it for lockfree. --- CODE_OF_CONDUCT.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 CODE_OF_CONDUCT.md diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md new file mode 100644 index 00000000..4366128c --- /dev/null +++ b/CODE_OF_CONDUCT.md @@ -0,0 +1,14 @@ +# Code of Conduct + +This project has adopted the [OCaml Code of Conduct](https://github.com/ocaml/code-of-conduct/blob/main/CODE_OF_CONDUCT.md). + +# Enforcement + +This project follows the OCaml Code of Conduct +[enforcement policy](https://github.com/ocaml/code-of-conduct/blob/main/CODE_OF_CONDUCT.md#enforcement). + +To report any violations, please contact: + +* Bartosz Modelski +* Carine Morel +* Sudha Parimala \ No newline at end of file From 087e287d86066edc90fe8d893fc03dd0273587c0 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 11 May 2023 14:31:16 +0200 Subject: [PATCH 11/22] Removing overlaps between github action and ocaml ci. Removing not working architecture. --- .github/workflows/main.yml | 24 +++++++++--------------- lockfree.opam | 1 + 2 files changed, 10 insertions(+), 15 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 3192d0a1..11efd986 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -8,17 +8,8 @@ on: - cron: 0 1 * * MON jobs: - build: - strategy: - matrix: - os: - - ubuntu-latest - - macos-latest - ocaml-compiler: - - ocaml-base-compiler.5.0.0 - - ocaml-variants.5.1.0+trunk - - runs-on: ${{ matrix.os }} + windows: + runs-on: windows-latest env: QCHECK_MSG_INTERVAL: '60' @@ -34,15 +25,18 @@ jobs: curl -sH "Accept: application/vnd.github.v3+json" \ https://api.github.com/repos/ocaml/ocaml/commits/trunk \ | jq .commit.tree.sha | xargs printf '::set-output name=commit::%s' + - name: Use OCaml ${{ matrix.ocaml-compiler }} uses: ocaml/setup-ocaml@v2 with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-pin: false + opam-depext: false + ocaml-compiler: ocaml.5.0.0,ocaml-option-mingw opam-repositories: | - default: https://github.com/ocaml/opam-repository.git - alpha: https://github.com/kit-ty-kate/opam-alpha-repository.git + dra27: https://github.com/dra27/opam-repository.git#windows-5.0 + default: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset + upstream: https://github.com/ocaml/opam-repository.git cache-prefix: ${{ steps.multicore_hash.outputs.commit }} - opam-depext: false - run: opam install . --deps-only --with-test diff --git a/lockfree.opam b/lockfree.opam index 0784d4d8..ebef0a6a 100644 --- a/lockfree.opam +++ b/lockfree.opam @@ -19,5 +19,6 @@ depends: [ "yojson" {>= "2.0.2"} "dscheck" {with-test & >= "0.0.1"} ] +available: arch != "x86_32" & arch != "arm32" & arch != "ppc64" depopts: [] build: ["dune" "build" "-p" name "-j" jobs] From a17d1a32a998002f87b00b5324aea3a33b995857 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 12 Jan 2023 11:20:36 +0100 Subject: [PATCH 12/22] Add multicoretest tests for current data structures. --- CHANGES.md | 8 +- lockfree.opam | 7 +- test/michael_scott_queue/dune | 7 ++ .../stm_michael_scott_queue.ml | 67 +++++++++++ test/mpsc_queue/dune | 7 ++ test/mpsc_queue/stm_mpsc_queue.ml | 112 ++++++++++++++++++ test/spsc_queue/dune | 7 ++ test/spsc_queue/stm_spsc_queue.ml | 87 ++++++++++++++ test/treiber_stack/dune | 7 ++ test/treiber_stack/stm_treiber_stack.ml | 67 +++++++++++ test/ws_deque/stm_ws_deque.ml | 56 ++------- 11 files changed, 384 insertions(+), 48 deletions(-) create mode 100644 test/michael_scott_queue/stm_michael_scott_queue.ml create mode 100644 test/mpsc_queue/stm_mpsc_queue.ml create mode 100644 test/spsc_queue/stm_spsc_queue.ml create mode 100644 test/treiber_stack/stm_treiber_stack.ml diff --git a/CHANGES.md b/CHANGES.md index d0ebc359..5600fcd8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,10 +2,14 @@ All notable changes to this project will be documented in this file. -## 0.3.1 +## Not released + +* Add STM tests for current data structures (@lyrm, @jmid) + +## 0.3.1 * Rework dscheck integration to work with utop (@lyrm) -* Add OCaml 4 compatability (@sudha247) +* Add OCaml 4 compatability (@sudha247) * Add STM ws_deque tests (@jmid, @lyrm) ## 0.3.0 diff --git a/lockfree.opam b/lockfree.opam index ebef0a6a..f78f4ba7 100644 --- a/lockfree.opam +++ b/lockfree.opam @@ -13,12 +13,15 @@ depends: [ "dune" {>= "3.0"} "domain_shims" {>= "0.1.0"} "qcheck" {with-test & >= "0.18.1"} - "qcheck-stm" {with-test & >= "0.1"} + "qcheck-stm" {with-test & >= "0.1.1"} "qcheck-alcotest" {with-test & >= "0.18.1"} "alcotest" {with-test & >= "1.6.0"} "yojson" {>= "2.0.2"} - "dscheck" {with-test & >= "0.0.1"} + "dscheck" {with-test & >= "0.1.0"} ] available: arch != "x86_32" & arch != "arm32" & arch != "ppc64" depopts: [] build: ["dune" "build" "-p" name "-j" jobs] +pin-depends: [ + [ "qcheck-stm.0.1.1" + "git+https://github.com/ocaml-multicore/multicoretests.git#4e2e1b22bffec3675a15cf6c2e05f733e9f8b66d" ] ] diff --git a/test/michael_scott_queue/dune b/test/michael_scott_queue/dune index 29deca1f..e89e28db 100644 --- a/test/michael_scott_queue/dune +++ b/test/michael_scott_queue/dune @@ -13,3 +13,10 @@ (name qcheck_michael_scott_queue) (libraries lockfree qcheck qcheck-alcotest) (modules qcheck_michael_scott_queue)) + +(test + (name stm_michael_scott_queue) + (modules stm_michael_scott_queue) + (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (action + (run %{test} --verbose))) diff --git a/test/michael_scott_queue/stm_michael_scott_queue.ml b/test/michael_scott_queue/stm_michael_scott_queue.ml new file mode 100644 index 00000000..a2c7ffaf --- /dev/null +++ b/test/michael_scott_queue/stm_michael_scott_queue.ml @@ -0,0 +1,67 @@ +(** Sequential and Parallel model-based tests of michael_scott_queue *) + +open QCheck +open STM +module Ms_queue = Lockfree.Michael_scott_queue + +module MSQConf = struct + type cmd = Push of int | Pop | Is_empty + + let show_cmd c = + match c with + | Push i -> "Push " ^ string_of_int i + | Pop -> "Pop" + | Is_empty -> "Is_empty" + + type state = int list + type sut = int Ms_queue.t + + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map (fun i -> Push i) int_gen; + Gen.return Pop; + Gen.return Is_empty; + ]) + + let init_state = [] + let init_sut () = Ms_queue.create () + let cleanup _ = () + + let next_state c s = + match c with + | Push i -> i :: s + | Pop -> ( match List.rev s with [] -> s | _ :: s' -> List.rev s') + | Is_empty -> s + + let precond _ _ = true + + let run c d = + match c with + | Push i -> Res (unit, Ms_queue.push d i) + | Pop -> Res (option int, Ms_queue.pop d) + | Is_empty -> Res (bool, Ms_queue.is_empty d) + + let postcond c (s : state) res = + match (c, res) with + | Push _, Res ((Unit, _), _) -> true + | Pop, Res ((Option Int, _), res) -> ( + match List.rev s with [] -> res = None | j :: _ -> res = Some j) + | Is_empty, Res ((Bool, _), res) -> res = (s = []) + | _, _ -> false +end + +module MSQ_seq = STM_sequential.Make (MSQConf) +module MSQ_dom = STM_domain.Make (MSQConf) + +let () = + let count = 500 in + QCheck_base_runner.run_tests_main + [ + MSQ_seq.agree_test ~count + ~name:"STM Lockfree.Michael_scott_queue test sequential"; + MSQ_dom.agree_test_par ~count + ~name:"STM Lockfree.Michael_scott_queue test parallel"; + ] diff --git a/test/mpsc_queue/dune b/test/mpsc_queue/dune index fa8bb40d..9776efd6 100644 --- a/test/mpsc_queue/dune +++ b/test/mpsc_queue/dune @@ -10,3 +10,10 @@ (name qcheck_mpsc_queue) (libraries lockfree qcheck qcheck-alcotest) (modules qcheck_mpsc_queue)) + +(test + (name stm_mpsc_queue) + (modules stm_mpsc_queue) + (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (action + (run %{test} --verbose))) diff --git a/test/mpsc_queue/stm_mpsc_queue.ml b/test/mpsc_queue/stm_mpsc_queue.ml new file mode 100644 index 00000000..83ecb40d --- /dev/null +++ b/test/mpsc_queue/stm_mpsc_queue.ml @@ -0,0 +1,112 @@ +(** Sequential and Parallel model-based tests of mpsc_queue *) + +open QCheck +open STM +open Util +module Mpsc_queue = Lockfree.Mpsc_queue + +module MPSCConf = struct + type cmd = Push of int | Pop | Push_head of int | Is_empty | Close + + let show_cmd c = + match c with + | Push i -> "Push " ^ string_of_int i + | Pop -> "Pop" + | Push_head i -> "Push_head" ^ string_of_int i + | Is_empty -> "Is_empty" + | Close -> "Close" + + type state = bool * int list + type sut = int Mpsc_queue.t + + let producer_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map (fun i -> Push i) int_gen; + Gen.return Is_empty; + Gen.return Close; + ]) + + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.return Pop; + Gen.map (fun i -> Push_head i) int_gen; + Gen.return Is_empty; + Gen.return Close; + ]) + + let init_state = (false, []) + let init_sut () = Mpsc_queue.create () + let cleanup _ = () + + let next_state c (is_closed, s) = + match c with + | Push i -> + (is_closed, if not is_closed then i :: List.rev s |> List.rev else s) + | Push_head i -> (is_closed, if not (is_closed && s = []) then i :: s else s) + | Is_empty -> (is_closed, s) + | Pop -> ( (is_closed, match s with [] -> s | _ :: s' -> s')) + | Close -> (true, s) + + let precond _ _ = true + + let run c d = + match c with + | Push i -> Res (result unit exn, protect (fun d -> Mpsc_queue.push d i) d) + | Pop -> Res (result (option int) exn, protect Mpsc_queue.pop d) + | Push_head i -> + Res (result unit exn, protect (fun d -> Mpsc_queue.push_head d i) d) + | Is_empty -> Res (result bool exn, protect Mpsc_queue.is_empty d) + | Close -> Res (result unit exn, protect Mpsc_queue.close d) + + let postcond c ((is_closed, s) : state) res = + match (c, res) with + | Push _, Res ((Result (Unit, Exn), _), res) -> + if is_closed then res = Error Mpsc_queue.Closed else res = Ok () + | Push_head _, Res ((Result (Unit, Exn), _), res) -> + if is_closed && s = [] then res = Error Mpsc_queue.Closed + else res = Ok () + | Pop, Res ((Result (Option Int, Exn), _), res) -> ( + match s with + | [] -> + if is_closed then res = Error Mpsc_queue.Closed else res = Ok None + | x :: _ -> res = Ok (Some x)) + | Is_empty, Res ((Result (Bool, Exn), _), res) -> + if is_closed && s = [] then res = Error Mpsc_queue.Closed + else res = Ok (s = []) + | Close, Res ((Result (Unit, Exn), _), res) -> + if is_closed then res = Error Mpsc_queue.Closed else res = Ok () + | _, _ -> false +end + +module MPSC_seq = STM_sequential.Make (MPSCConf) +module MPSC_dom = STM_domain.Make (MPSCConf) + +(* [arb_cmds_par] differs in what each triple component generates: + "Consumer domain" cmds can't be [Push] (but can be [Pop], [Is_empty], [Close] or [Push_head]), + "producer domain" cmds can't be [Push_head] or [Pop] (but can be [Push], [Is_empty] or [Close]). *) +let arb_cmds_par = + MPSC_dom.arb_triple 20 12 MPSCConf.arb_cmd MPSCConf.arb_cmd + MPSCConf.producer_cmd + +(* A parallel agreement test - w/repeat and retries combined *) +let agree_test_par_asym ~count ~name = + let rep_count = 50 in + Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple -> + assume (MPSC_dom.all_interleavings_ok triple); + repeat rep_count MPSC_dom.agree_prop_par_asym triple) + +let () = + let count = 1000 in + QCheck_base_runner.run_tests_main + [ + MPSC_seq.agree_test ~count ~name:"STM Lockfree.Mpsc_queue test sequential"; + agree_test_par_asym ~count ~name:"STM Lockfree.Mpsc_queue test parallel"; + MPSC_dom.neg_agree_test_par ~count + ~name:"STM Lockfree.Mpsc_queue test parallel, negative"; + ] diff --git a/test/spsc_queue/dune b/test/spsc_queue/dune index 718d6e50..9bf002b1 100644 --- a/test/spsc_queue/dune +++ b/test/spsc_queue/dune @@ -15,3 +15,10 @@ (name qcheck_spsc_queue) (libraries lockfree qcheck "qcheck-alcotest") (modules qcheck_spsc_queue)) + +(test + (name stm_spsc_queue) + (modules stm_spsc_queue) + (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (action + (run %{test} --verbose))) diff --git a/test/spsc_queue/stm_spsc_queue.ml b/test/spsc_queue/stm_spsc_queue.ml new file mode 100644 index 00000000..d8d01c51 --- /dev/null +++ b/test/spsc_queue/stm_spsc_queue.ml @@ -0,0 +1,87 @@ +(** Sequential and Parallel model-based tests of spsc_queue *) + +open QCheck +open STM +open Util +module Spsc_queue = Lockfree.Spsc_queue + +module SPSCConf = struct + type cmd = Push of int | Pop + + let show_cmd c = + match c with Push i -> "Push " ^ string_of_int i | Pop -> "Pop" + + type state = int * int list + type sut = int Spsc_queue.t + + let producer_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd (Gen.map (fun i -> Push i) int_gen) + + let consumer_cmd _s = QCheck.make ~print:show_cmd (Gen.return Pop) + + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof [ Gen.return Pop; Gen.map (fun i -> Push i) int_gen ]) + + let size_exponent = 4 + let max_size = Int.shift_left 1 size_exponent + let init_state = (0, []) + let init_sut () = Spsc_queue.create ~size_exponent + let cleanup _ = () + + let next_state c (n, s) = + match c with + | Push i -> if n = max_size then (n, s) else (n + 1, i :: s) + | Pop -> ( + match List.rev s with [] -> (0, s) | _ :: s' -> (n - 1, List.rev s')) + + let precond _ _ = true + + let run c d = + match c with + | Push i -> Res (result unit exn, protect (fun d -> Spsc_queue.push d i) d) + | Pop -> Res (result (option int) exn, protect Spsc_queue.pop d) + + let postcond c ((n, s) : state) res = + match (c, res) with + | Push _, Res ((Result (Unit, Exn), _), res) -> ( + match res with + | Error Spsc_queue.Full -> n = max_size + | Ok () -> n < max_size + | _ -> false) + | Pop, Res ((Result (Option Int, Exn), _), res) -> ( + match (res, List.rev s) with + | Ok None, [] -> true + | Ok (Some j), x :: _ -> x = j + | _ -> false) + | _, _ -> false +end + +module SPSC_seq = STM_sequential.Make (SPSCConf) +module SPSC_dom = STM_domain.Make (SPSCConf) + +(* [arb_cmds_par] differs in what each triple component generates: + "Producer domain" cmds can't be [Pop], "consumer domain" cmds can only be [Pop]. *) +let arb_cmds_par = + SPSC_dom.arb_triple 20 12 SPSCConf.producer_cmd SPSCConf.producer_cmd + SPSCConf.consumer_cmd + +(* A parallel agreement test - w/repeat and retries combined *) +let agree_test_par_asym ~count ~name = + let rep_count = 20 in + Test.make ~retries:10 ~count ~name arb_cmds_par (fun triple -> + assume (SPSC_dom.all_interleavings_ok triple); + repeat rep_count SPSC_dom.agree_prop_par_asym triple) + +let () = + let count = 1000 in + QCheck_base_runner.run_tests_main + [ + SPSC_seq.agree_test ~count ~name:"STM Lockfree.Spsc_queue test sequential"; + agree_test_par_asym ~count ~name:"STM Lockfree.Spsc_queue test parallel"; + (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) + SPSC_dom.neg_agree_test_par ~count + ~name:"STM Lockfree.Spsc_queue test parallel, negative"; + ] diff --git a/test/treiber_stack/dune b/test/treiber_stack/dune index 9561de95..841cf9eb 100644 --- a/test/treiber_stack/dune +++ b/test/treiber_stack/dune @@ -13,3 +13,10 @@ (name qcheck_treiber_stack) (libraries lockfree qcheck qcheck-alcotest) (modules qcheck_treiber_stack)) + +(test + (name stm_treiber_stack) + (modules stm_treiber_stack) + (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (action + (run %{test} --verbose))) diff --git a/test/treiber_stack/stm_treiber_stack.ml b/test/treiber_stack/stm_treiber_stack.ml new file mode 100644 index 00000000..2a4a5b1f --- /dev/null +++ b/test/treiber_stack/stm_treiber_stack.ml @@ -0,0 +1,67 @@ +(** Sequential and Parallel model-based tests of treiber_stack *) + +open QCheck +open STM +module Treiber_stack = Lockfree.Treiber_stack + +module TSConf = struct + type cmd = Push of int | Pop | Is_empty + + let show_cmd c = + match c with + | Push i -> "Push " ^ string_of_int i + | Pop -> "Pop" + | Is_empty -> "Is_empty" + + type state = int list + type sut = int Treiber_stack.t + + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map (fun i -> Push i) int_gen; + Gen.return Pop; + Gen.return Is_empty; + ]) + + let init_state = [] + let init_sut () = Treiber_stack.create () + let cleanup _ = () + + let next_state c s = + match c with + | Push i -> i :: s + | Pop -> ( match s with [] -> s | _ :: s' -> s') + | Is_empty -> s + + let precond _ _ = true + + let run c d = + match c with + | Push i -> Res (unit, Treiber_stack.push d i) + | Pop -> Res (option int, Treiber_stack.pop d) + | Is_empty -> Res (bool, Treiber_stack.is_empty d) + + let postcond c (s : state) res = + match (c, res) with + | Push _, Res ((Unit, _), _) -> true + | Pop, Res ((Option Int, _), res) -> ( + match s with [] -> res = None | j :: _ -> res = Some j) + | Is_empty, Res ((Bool, _), res) -> res = (s = []) + | _, _ -> false +end + +module TS_seq = STM_sequential.Make (TSConf) +module TS_dom = STM_domain.Make (TSConf) + +let () = + let count = 500 in + QCheck_base_runner.run_tests_main + [ + TS_seq.agree_test ~count + ~name:"STM Lockfree.Treiber_stack test sequential"; + TS_dom.agree_test_par ~count + ~name:"STM Lockfree.Treiber_stack test parallel"; + ] diff --git a/test/ws_deque/stm_ws_deque.ml b/test/ws_deque/stm_ws_deque.ml index fd502bc6..4eb91c7e 100644 --- a/test/ws_deque/stm_ws_deque.ml +++ b/test/ws_deque/stm_ws_deque.ml @@ -63,56 +63,24 @@ end module WSDT_seq = STM_sequential.Make (WSDConf) module WSDT_dom = STM_domain.Make (WSDConf) -(* The following definitions differ slightly from those in multicoretests:lib/STM.ml. - This has to do with how work-stealing deques are supposed to be used according to spec: - - [agree_prop_par] differs in that it only spawns one domain ("a stealer domain") - in parallel with the original "owner domain" (it also uses [Semaphore.Binary]) *) -let agree_prop_par (seq_pref, owner, stealer) = - assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ owner)); - assume (WSDT_seq.cmds_ok WSDConf.init_state (seq_pref @ stealer)); - let sut = WSDConf.init_sut () in - let pref_obs = WSDT_dom.interp_sut_res sut seq_pref in - let sema = Semaphore.Binary.make false in - let stealer_dom = - Domain.spawn (fun () -> - Semaphore.Binary.release sema; - WSDT_dom.interp_sut_res sut stealer) - in - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; - let own_obs = WSDT_dom.interp_sut_res sut owner in - let stealer_obs = Domain.join stealer_dom in - let res = - WSDT_dom.check_obs pref_obs own_obs stealer_obs WSDConf.init_state - in - let () = WSDConf.cleanup sut in - res - || Test.fail_reportf " Results incompatible with linearized model:\n\n%s" - @@ Util.print_triple_vertical ~center_prefix:false STM.show_res - (List.map snd pref_obs, List.map snd own_obs, List.map snd stealer_obs) - -(* [arb_cmds_par] differs in what each triple component generates: - "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *) -let arb_cmds_par = - WSDT_dom.arb_triple 20 15 WSDConf.arb_cmd WSDConf.arb_cmd WSDConf.stealer_cmd - (* A parallel agreement test - w/repeat and retries combined *) -let agree_test_par ~count ~name = - let rep_count = 50 in - Test.make ~retries:10 ~count ~name arb_cmds_par - (repeat rep_count agree_prop_par) - -(* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) -let agree_test_par_negative ~count ~name = - WSDT_dom.neg_agree_test_par ~count ~name +let agree_test_par_asym ~count ~name = + let rep_count = 20 in + let seq_len, par_len = (20, 12) in + Test.make ~retries:10 ~count ~name + (* "Owner domain" cmds can't be [Steal], "stealer domain" cmds can only be [Steal]. *) + (WSDT_dom.arb_triple_asym seq_len par_len WSDConf.arb_cmd WSDConf.arb_cmd + WSDConf.stealer_cmd) (fun triple -> + assume (WSDT_dom.all_interleavings_ok triple); + repeat rep_count WSDT_dom.agree_prop_par_asym triple) let () = let count = 1000 in QCheck_base_runner.run_tests_main [ WSDT_seq.agree_test ~count ~name:"STM Lockfree.Ws_deque test sequential"; - agree_test_par ~count ~name:"STM Lockfree.Ws_deque test parallel"; - agree_test_par_negative ~count + agree_test_par_asym ~count ~name:"STM Lockfree.Ws_deque test parallel"; + (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) + WSDT_dom.neg_agree_test_par ~count ~name:"STM Lockfree.Ws_deque test parallel, negative"; ] From d87aca188879f6a062926a0dc17925cdf64f072d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 2 Jun 2023 13:07:01 +0200 Subject: [PATCH 13/22] Require qcheck-stm.0.2 and remove pin --- lockfree.opam | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/lockfree.opam b/lockfree.opam index f78f4ba7..8b1fa0cf 100644 --- a/lockfree.opam +++ b/lockfree.opam @@ -13,7 +13,7 @@ depends: [ "dune" {>= "3.0"} "domain_shims" {>= "0.1.0"} "qcheck" {with-test & >= "0.18.1"} - "qcheck-stm" {with-test & >= "0.1.1"} + "qcheck-stm" {with-test & >= "0.2"} "qcheck-alcotest" {with-test & >= "0.18.1"} "alcotest" {with-test & >= "1.6.0"} "yojson" {>= "2.0.2"} @@ -22,6 +22,3 @@ depends: [ available: arch != "x86_32" & arch != "arm32" & arch != "ppc64" depopts: [] build: ["dune" "build" "-p" name "-j" jobs] -pin-depends: [ - [ "qcheck-stm.0.1.1" - "git+https://github.com/ocaml-multicore/multicoretests.git#4e2e1b22bffec3675a15cf6c2e05f733e9f8b66d" ] ] From a782481f8f0ece5718f31423463460f3ecafce0d Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 23 Feb 2023 14:30:43 +0100 Subject: [PATCH 14/22] - Renaming lockfree to Saturn - Change data structures names for user-ergonomy (treiber_stack -> stack for example) - Uniformize queue interface and doc - Add CONTRIBUTING file and complete test/README.md --- .gitignore | 4 +- .ocamlformat | 2 +- .prettierrc | 14 +++ CHANGES.md | 23 ++--- CONTRIBUTING.md | 30 ++++++ README.md | 45 +++++---- bench/README.md | 12 ++- bench/backoff.ml | 8 +- bench/bench_spsc_queue.ml | 2 +- bench/dune | 2 +- bench/main.ml | 2 +- bench/mpmc_queue.ml | 6 +- bench/orchestrator.mli | 31 ++++++- dune-project | 2 +- lockfree.opam => saturn.opam | 12 +-- seqtest/dune | 2 +- seqtest/seqtest.ml | 2 +- src/dune | 4 +- src/michael_scott_queue.mli | 15 +-- src/mpmc_relaxed_queue.mli | 42 ++++----- src/mpsc_queue.mli | 40 +++++--- src/{lockfree.ml => saturn.ml} | 13 +-- src/{lockfree.mli => saturn.mli} | 23 +++-- src/spsc_queue.mli | 21 +++-- src/treiber_stack.mli | 15 +-- src/ws_deque.mli | 40 ++++---- test/README.md | 75 ++++++++++++++- test/michael_scott_queue/dune | 4 +- .../qcheck_michael_scott_queue.ml | 49 +++++----- .../stm_michael_scott_queue.ml | 6 +- test/mpmc_relaxed_queue/dune | 2 +- .../test_mpmc_relaxed_queue.ml | 91 ++++++++++--------- test/mpsc_queue/dune | 4 +- test/mpsc_queue/qcheck_mpsc_queue.ml | 2 +- test/mpsc_queue/stm_mpsc_queue.ml | 8 +- test/spsc_queue/dune | 6 +- test/spsc_queue/qcheck_spsc_queue.ml | 2 +- test/spsc_queue/stm_spsc_queue.ml | 8 +- test/spsc_queue/test_spsc_queue.ml | 2 +- test/treiber_stack/dune | 4 +- test/treiber_stack/qcheck_treiber_stack.ml | 48 +++++----- test/treiber_stack/stm_treiber_stack.ml | 7 +- test/ws_deque/dune | 6 +- test/ws_deque/qcheck_ws_deque.ml | 2 +- test/ws_deque/stm_ws_deque.ml | 8 +- test/ws_deque/test_ws_deque.ml | 2 +- 46 files changed, 464 insertions(+), 284 deletions(-) create mode 100644 .prettierrc create mode 100644 CONTRIBUTING.md rename lockfree.opam => saturn.opam (59%) rename src/{lockfree.ml => saturn.ml} (85%) rename src/{lockfree.mli => saturn.mli} (80%) diff --git a/.gitignore b/.gitignore index 63b850eb..7fbb1ea4 100644 --- a/.gitignore +++ b/.gitignore @@ -6,4 +6,6 @@ tmp *.install *.native *.byte -*.merlin \ No newline at end of file +*.merlin +*.json +node_modules \ No newline at end of file diff --git a/.ocamlformat b/.ocamlformat index daa1fc92..13941e32 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,2 +1,2 @@ profile = default -version = 0.23.0 +version = 0.25.1 diff --git a/.prettierrc b/.prettierrc new file mode 100644 index 00000000..27d57608 --- /dev/null +++ b/.prettierrc @@ -0,0 +1,14 @@ +{ + "arrowParens": "avoid", + "bracketSpacing": false, + "printWidth": 80, + "semi": false, + "singleQuote": true, + "proseWrap": "always", + "overrides": [ + { + "files": ["*.md"], + "excludeFiles": "_build/*" + } + ] +} diff --git a/CHANGES.md b/CHANGES.md index 5600fcd8..0480fabb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,23 +4,24 @@ All notable changes to this project will be documented in this file. ## Not released -* Add STM tests for current data structures (@lyrm, @jmid) +- Rename data structures and package, add docs (@lyrm) +- Add STM tests for current data structures (@lyrm, @jmid) ## 0.3.1 -* Rework dscheck integration to work with utop (@lyrm) -* Add OCaml 4 compatability (@sudha247) -* Add STM ws_deque tests (@jmid, @lyrm) +- Rework dscheck integration to work with utop (@lyrm) +- Add OCaml 4 compatability (@sudha247) +- Add STM ws_deque tests (@jmid, @lyrm) ## 0.3.0 -* Add MPSC queue (@lyrm) -* Add SPSC queue (@bartoszmodelski) -* Add MPMC relaxed queue (@bartoszmodelski, @lyrm) -* Add Michael-Scott Queue (@tmcgilchrist, @bartoszmodelski, @lyrm) -* Add Treiber Stack (@tmcgilchrist , @bartoszmodelski, @lyrm) -* Integrate model-checker (DSCheck) (@bartoszmodelski) +- Add MPSC queue (@lyrm) +- Add SPSC queue (@bartoszmodelski) +- Add MPMC relaxed queue (@bartoszmodelski, @lyrm) +- Add Michael-Scott Queue (@tmcgilchrist, @bartoszmodelski, @lyrm) +- Add Treiber Stack (@tmcgilchrist , @bartoszmodelski, @lyrm) +- Integrate model-checker (DSCheck) (@bartoszmodelski) ## v0.2.0 -* Add Chase-Lev Work-stealing deque `Ws_deque`. (@ctk21) +- Add Chase-Lev Work-stealing deque `Ws_deque`. (@ctk21) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 00000000..d2864645 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,30 @@ +## Contributing + +Any contributions are appreciated! Please create issues/PRs to this repo. + +### Maintainers + +The current list of maintainers is as follows: + +- @kayceesrk KC Sivaramakrishnan +- @lyrm Carine Morel +- @Sudha247 Sudha Parimala + +### Guidelines for new data structures implementation + +Reviewing most implementation takes times. Here are a few guidelines to make it +easier for the reviewers : + +- the issue tracker has a good list of data structures to choose from +- implement a well know algorithm (there are a lot !) + - from a _reviewed_ paper, ideally with proof of main claimed properties (like + lock-freedom, deadlock freedom etc..) + - from a well known and used concurrent library (like `java.util.concurrent`) +- write tests with **multiple** domains. All the following tests are expected to + be provided before a proper review is done, especially for implementations + that do not come from a well-know algorithm : + - unitary tests and `qcheck tests` : with one and multiple domains. If domains + have specific roles (producer, consumer, stealer, etc..), it should appear + in the tests. + - tests using `STM` from `multicoretest` + - (_optional_) `dscheck` tests (for non-blocking implementation) diff --git a/README.md b/README.md index 15022e88..2ad2ef6b 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,21 @@ -# `lockfree` — Lock-free data structures for Multicore OCaml --------------------------------------------------------- +# `Saturn` — parallelism-safe data structures for Multicore OCaml -A collection of Concurrent Lockfree Data Structures for OCaml 5. It contains: +--- -* [Treiber Stack](src/treiber_stack.mli) A classic multi-producer multi-consumer stack, robust and flexible. Recommended starting point when needing LIFO structure. - -* [Michael-Scott Queue](src/michael_scott_queue.mli) A classic multi-producer multi-consumer queue, robust and flexible. Recommended starting point when needing FIFO structure. It is based on [Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms](https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf). +A collection of parallelism-safe data structures for OCaml 5. It contains: -* [Chase-Lev Work-Stealing Deque](src/ws_deque.mli) Single-producer, multi-consumer dynamic-size double-ended queue (deque) (see [Dynamic circular work-stealing deque](https://dl.acm.org/doi/10.1145/1073970.1073974) and [Correct and efficient work-stealing for weak memory models](https://dl.acm.org/doi/abs/10.1145/2442516.2442524)). Ideal for throughput-focused scheduling using per-core work distribution. Note, [pop] and [steal] follow different ordering (respectively LIFO and FIFO) and have different linearization contraints. - -* [SPSC Queue](src/spsc_queue.mli) Simple single-producer single-consumer fixed-size queue. Thread-safe as long as at most one thread acts as producer and at most one as consumer at any single point in time. - -* [MPMC Relaxed Queue](src/mpmc_relaxed_queue.mli) Multi-producer, multi-consumer, fixed-size relaxed queue. Optimised for high number of threads. Not strictly FIFO. Note, it exposes two interfaces: a lockfree and a non-lockfree (albeit more practical) one. See the mli for details. - -* [MPSC Queue](src/mpsc_queue.mli) A multi-producer, single-consumer, thread-safe queue without support for cancellation. This makes a good data structure for a scheduler's run queue. It is used in [Eio](https://github.com/ocaml-multicore/eio). It is a single consumer version of the queue described in [Implementing lock-free queues](https://people.cs.pitt.edu/~jacklange/teaching/cs2510-f12/papers/implementing_lock_free.pdf). +| Name | What is it ? | Sources | +| -------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| [Treiber Stack](src/treiber_stack.mli) | A classic multi-producer multi-consumer stack, robust and flexible. Recommended starting point when needing LIFO structure | | +| [Michael-Scott Queue](src/michael_scott_queue.mli) | A classic multi-producer multi-consumer queue, robust and flexible. Recommended starting point when needing FIFO structure. | [Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms](https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf) | +| [Chase-Lev Work-Stealing Deque](src/ws_deque.mli) | Single-producer, multi-consumer dynamic-size double-ended queue (deque). Ideal for throughput-focused scheduling using per-core work distribution. Note, `pop` and `steal` follow different ordering (respectively LIFO and FIFO) and have different linearization contraints. | [Dynamic circular work-stealing deque](https://dl.acm.org/doi/10.1145/1073970.1073974) and [Correct and efficient work-stealing for weak memory models](https://dl.acm.org/doi/abs/10.1145/2442516.2442524)) | +| [SPSC Queue](src/spsc_queue.mli) | Simple single-producer single-consumer fixed-size queue. Thread-safe as long as at most one thread acts as producer and at most one as consumer at any single point in time. | | +| [MPMC Relaxed Queue](src/mpmc_relaxed_queue.mli) | Multi-producer, multi-consumer, fixed-size relaxed queue. Optimised for high number of threads. Not strictly FIFO. Note, it exposes two interfaces: a lockfree and a non-lockfree (albeit more practical) one. See the mli for details. | | +| [MPSC Queue](src/mpsc_queue.mli) | A multi-producer, single-consumer, thread-safe queue without support for cancellation. This makes a good data structure for a scheduler's run queue. It is used in [Eio](https://github.com/ocaml-multicore/eio). | It is a single consumer version of the queue described in [Implementing lock-free queues](https://people.cs.pitt.edu/~jacklange/teaching/cs2510-f12/papers/implementing_lock_free.pdf). | ## Usage -lockfree can be installed from `opam`: `opam install lockfree`. Sample usage of +`Saturn` can be installed from `opam`: `opam install saturn`. Sample usage of `Ws_deque` is illustrated below. ```ocaml @@ -30,11 +28,26 @@ let () = Ws_deque.push q 100 let () = assert (Ws_deque.pop q = 100) ``` +## Tests + +Several kind of tests are provided for each data structure: + +- unitary tests and `qcheck` tests: check semantics and expected behaviors with + one and more domains; +- `STM` tests: check _linearizability_ for two domains (see + [multicoretests library](https://github.com/ocaml-multicore/multicoretests)); +- `dscheck`: checks _non-blocking_ property for as many domains as wanted (for + two domains most of the time). See + [dscheck](https://github.com/ocaml-multicore/dscheck). + +See [test/README.md](test/README.md) for more details. + ## Benchmarks -There is a number of benchmarks in `bench/` directory. You can run them with `make bench`. See [bench/README.md](bench/README.md) for more details. +There is a number of benchmarks in `bench` directory. You can run them with +`make bench`. See [bench/README.md](bench/README.md) for more details. ## Contributing -Contributions of more lockfree data structures appreciated! Please create +Contributions of more parallelism-safe data structures appreciated! Please create issues/PRs to this repo. diff --git a/bench/README.md b/bench/README.md index 71ce8284..0f71fd12 100644 --- a/bench/README.md +++ b/bench/README.md @@ -1,11 +1,13 @@ -Benchmarks for lockfree +Benchmarks for Saturn -# General usage +# General usage -Execute `make bench` from root of the repository to run the standard set of benchmarks. The output is in JSON, as it is intended to be consumed by ocaml-benchmark CI (in progress). +Execute `make bench` from root of the repository to run the standard set of +benchmarks. The output is in JSON, as it is intended to be consumed by +ocaml-benchmark CI (in progress). -# Specific structures +# Specific structures Some benchmarks expose commandline interface targeting particular structures: -* [mpmc_queue.exe](mpmc_queue_cmd.ml) \ No newline at end of file +- [mpmc_queue.exe](mpmc_queue_cmd.ml) diff --git a/bench/backoff.ml b/bench/backoff.ml index ac5ab5b6..06520053 100644 --- a/bench/backoff.ml +++ b/bench/backoff.ml @@ -5,7 +5,7 @@ type 'a t = { value : 'a; next : 'a t option Atomic.t } let empty () = { value = Obj.magic (); next = Atomic.make None } let push ~backoff_once t value = - let b = Lockfree.Backoff.create () in + let b = Saturn.Backoff.create () in let new_head = ({ value; next = Atomic.make None } : 'a t) in let rec push_f () = let head = Atomic.get t.next in @@ -18,7 +18,7 @@ let push ~backoff_once t value = push_f () let rec pop ?min_wait ~backoff_once t = - let b = Lockfree.Backoff.create ?min_wait () in + let b = Saturn.Backoff.create ?min_wait () in let head = Atomic.get t.next in match head with | None -> None @@ -95,8 +95,8 @@ let run_artificial ~backoff_once () = let bench ~run_type ~with_backoff () = let backoff_once = - if with_backoff then Lockfree.Backoff.once - else fun (_ : Lockfree.Backoff.t) -> () + if with_backoff then Saturn.Backoff.once + else fun (_ : Saturn.Backoff.t) -> () in let results = ref [] in let run = diff --git a/bench/bench_spsc_queue.ml b/bench/bench_spsc_queue.ml index 7ca6e2ee..6d7a823c 100644 --- a/bench/bench_spsc_queue.ml +++ b/bench/bench_spsc_queue.ml @@ -1,4 +1,4 @@ -open Lockfree +module Spsc_queue = Saturn.Single_prod_single_cons_queue let item_count = 2_000_000 diff --git a/bench/dune b/bench/dune index 824a8020..3e5cb1b2 100644 --- a/bench/dune +++ b/bench/dune @@ -1,3 +1,3 @@ (executables (names main mpmc_queue_cmd) - (libraries lockfree unix yojson)) + (libraries saturn unix yojson)) diff --git a/bench/main.ml b/bench/main.ml index c6474cb9..9c78237e 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -27,7 +27,7 @@ let () = |> String.concat ", " in let output = - Printf.sprintf {| {"name": "lockfree", "results": [%s]}|} results + Printf.sprintf {| {"name": "saturn", "results": [%s]}|} results (* Cannot use Yojson rewriters as of today none works on OCaml 5.1.0. This at least verifies that the manually crafted JSON is well-formed. diff --git a/bench/mpmc_queue.ml b/bench/mpmc_queue.ml index 2c919d15..1300145a 100644 --- a/bench/mpmc_queue.ml +++ b/bench/mpmc_queue.ml @@ -1,4 +1,4 @@ -open Lockfree.Mpmc_relaxed_queue +open Saturn.Relaxed_queue let num_of_elements = ref 500_000 let num_of_pushers = ref 4 @@ -57,8 +57,8 @@ let create_output ~time_median ~throughput_median ~throughput_stddev = let run_bench () = if !use_cas_intf then ( - push := Lockfree.Mpmc_relaxed_queue.Not_lockfree.CAS_interface.push; - pop := Lockfree.Mpmc_relaxed_queue.Not_lockfree.CAS_interface.pop); + push := Saturn.Relaxed_queue.Not_lockfree.CAS_interface.push; + pop := Saturn.Relaxed_queue.Not_lockfree.CAS_interface.pop); let queue = create ~size_exponent:10 () in let orchestrator = Orchestrator.init diff --git a/bench/orchestrator.mli b/bench/orchestrator.mli index 0e29ddfd..074f57b5 100644 --- a/bench/orchestrator.mli +++ b/bench/orchestrator.mli @@ -1,8 +1,37 @@ -(** Helper library that ensures all workers have started before any +(** Helper library that ensures all workers have started before any starts making progress on the benchmark. *) type t +(** An orchestrator is similar to a counter that ensures each domain + has started and complete each round simultanously. All domains + wait for the other before beginning the next round. *) val init : total_domains:int -> rounds:int -> t +(** [init ~total_domains:nd ~rounds:nr] create an orchestrator that + will run [nr] rounds for a test that uses exactly [nd] worker + domains *) + val worker : t -> (unit -> unit) -> unit +(** [worker t f] builds the function to pass to [Domain.spawn] while + using the orchestrator [t]. Doing [Domain.spawn (fun () -> worker + t f)] is similar to [Domain.spawn f] except that the orchestrator + is used to synchronize all domains progress. + *) + val run : ?drop_first:bool -> t -> float List.t +(** [run t] is launching the benchmark by enabling domains to progress. Benchmarks code should have the following structure : + +{[ + (* Initialize the orchestrator, with [nd] the number of domains we want. *) + let orchestrator = init ~total_domain:nd ~round:100 in + (* Spawn domains with [worker] *) + let domains = + List.init nd (fun _ -> + Domain.spawn (fun () -> + worker orchestrator (fun () -> some_function ()))) in + (* Run the benchmarks by freeing domains round by round. *) + let times = run orchestrator in + ... +]} + +*) diff --git a/dune-project b/dune-project index 8f376aa5..c50ca2f8 100644 --- a/dune-project +++ b/dune-project @@ -1,2 +1,2 @@ (lang dune 3.0) -(name lockfree) +(name saturn) diff --git a/lockfree.opam b/saturn.opam similarity index 59% rename from lockfree.opam rename to saturn.opam index 8b1fa0cf..4947d89e 100644 --- a/lockfree.opam +++ b/saturn.opam @@ -1,12 +1,12 @@ opam-version: "2.0" -maintainer: "KC Sivaramakrishnan " +maintainer:"KC Sivaramakrishnan " authors: ["KC Sivaramakrishnan "] -homepage: "https://github.com/ocaml-multicore/lockfree" -doc: "https://ocaml-multicore.github.io/lockfree" -synopsis: "Lock-free data structures for multicore OCaml" +homepage: "https://github.com/ocaml-multicore/saturn" +doc: "https://ocaml-multicore.github.io/saturn" +synopsis: "Parallelism-safe data structures for multicore OCaml" license: "ISC" -dev-repo: "git+https://github.com/ocaml-multicore/lockfree.git" -bug-reports: "https://github.com/ocaml-multicore/lockfree/issues" +dev-repo: "git+https://github.com/ocaml-multicore/saturn.git" +bug-reports: "https://github.com/ocaml-multicore/saturn/issues" tags: [] depends: [ "ocaml" {>= "4.12"} diff --git a/seqtest/dune b/seqtest/dune index 078eddc5..a5eb461b 100644 --- a/seqtest/dune +++ b/seqtest/dune @@ -1,6 +1,6 @@ (executable (name seqtest) - (libraries monolith lockfree) + (libraries monolith saturn) (modules seqtest) (enabled_if (= %{profile} seqtest))) diff --git a/seqtest/seqtest.ml b/seqtest/seqtest.ml index 4637a082..12b9ed00 100644 --- a/seqtest/seqtest.ml +++ b/seqtest/seqtest.ml @@ -1,5 +1,5 @@ open Monolith -open Lockfree.Ws_deque +open Saturn.Work_stealing_deque (* This sequential implementation of stacks serves as a reference. *) diff --git a/src/dune b/src/dune index 5d23de5a..efb4216d 100644 --- a/src/dune +++ b/src/dune @@ -1,4 +1,4 @@ (library - (name lockfree) - (public_name lockfree) + (name saturn) + (public_name saturn) (libraries domain_shims)) diff --git a/src/michael_scott_queue.mli b/src/michael_scott_queue.mli index 24243f42..88090256 100644 --- a/src/michael_scott_queue.mli +++ b/src/michael_scott_queue.mli @@ -16,9 +16,10 @@ *) (** - Michael-Scott Queue. A classic multi-producer multi-consumer queue, - robust and flexible. Recommended starting point when needing FIFO - structure. It is inspired by {{: + Michael-Scott classic multi-producer multi-consumer queue. + + All functions are lockfree. It is the recommended starting point + when needing FIFO structure. It is inspired by {{: https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms}. @@ -28,17 +29,17 @@ type 'a t (** The type of lock-free queue. *) val create : unit -> 'a t -(** Create a new queue, which is initially empty. *) +(** [create ()] returns a new queue, initially empty. *) val is_empty : 'a t -> bool (** [is_empty q] returns empty if [q] is empty. *) val push : 'a t -> 'a -> unit -(** [push q v] pushes [v] to the back of the queue. *) +(** [push q v] adds the element [v] at the end of the queue [q]. *) val pop : 'a t -> 'a option -(** [pop q] pops an element [e] from the front of the queue and returns - [Some v] if the queue is non-empty. Otherwise, returns [None]. *) +(** [pop q] removes and returns the first element in queue [q], or + returns [None] if the queue is empty. *) val clean_until : 'a t -> ('a -> bool) -> unit (** [clean_until q f] drops the prefix of the queue until the element [e], diff --git a/src/mpmc_relaxed_queue.mli b/src/mpmc_relaxed_queue.mli index 47e1fda6..235fa36b 100644 --- a/src/mpmc_relaxed_queue.mli +++ b/src/mpmc_relaxed_queue.mli @@ -1,18 +1,18 @@ -(** - A lock-free multi-producer, multi-consumer, thread-safe, relaxed-FIFO queue. +(** + A multi-producer, multi-consumer, thread-safe, relaxed-FIFO queue. - It exposes two interfaces: [Spin] and [Not_lockfree]. [Spin] is lock-free - formally, but the property is achieved in a fairly counterintuitive way - + It exposes two interfaces: [Spin] and [Not_lockfree]. [Spin] is lock-free + formally, but the property is achieved in a fairly counterintuitive way - - by using the fact that lock-freedom does not impose any constraints on - partial methods. In simple words, an invocation of function that cannot - logically terminate (`push` on full queue, `pop` on empty queue), it is - allowed to *busy-wait* until the precondition is meet. + partial methods. In simple words, an invocation of function that cannot + logically terminate (`push` on full queue, `pop` on empty queue), it is + allowed to *busy-wait* until the precondition is meet. - Above interface is impractical outside specialized applications. Thus, - [Mpmc_relaxed_queue] also exposes [Not_lockfree] interface. [Not_lockfree] - contains non-lockfree paths. While formally a locked algorithm, it will - often be the more practical solution as it allows having an overflow - queue, etc. + Above interface is impractical outside specialized applications. Thus, + [Mpmc_relaxed_queue] also exposes [Not_lockfree] interface. [Not_lockfree] + contains non-lockfree paths. While formally a locked algorithm, it will + often be the more practical solution as it allows having an overflow + queue, etc. *) type 'a t = private { @@ -28,22 +28,22 @@ val create : size_exponent:int -> unit -> 'a t [2^size_exponent]. *) module Spin : sig - (** [Spin] exposes a formally lock-free interface as per the [A lock-free relaxed - concurrent queue for fast work distribution] paper. Functions here busy-wait if + (** [Spin] exposes a formally lock-free interface as per the [A lock-free relaxed + concurrent queue for fast work distribution] paper. Functions here busy-wait if the action cannot be completed (i.e. [push] on full queue, [pop] on empty queue). *) val push : 'a t -> 'a -> unit - (** [push t x] adds [x] to the tail of the queue. If the queue is full, [push] + (** [push t x] adds [x] to the tail of the queue. If the queue is full, [push] busy-waits until another thread removes an item. *) val pop : 'a t -> 'a - (** [pop t] removes an item from the head of the queue. If the queue is empty, + (** [pop t] removes an item from the head of the queue. If the queue is empty, [pop] busy-waits until an item appear. *) end module Not_lockfree : sig - (** [Non_lockfree] exposes an interface that contains non-lockfree paths, i.e. threads - may need to cooperate to terminate. It is often more practical than [Spin], in + (** [Non_lockfree] exposes an interface that contains non-lockfree paths, i.e. threads + may need to cooperate to terminate. It is often more practical than [Spin], in particular when using a fair OS scheduler. *) val push : 'a t -> 'a -> bool @@ -55,10 +55,10 @@ module Not_lockfree : sig Returns [None] if [t] is currently empty. *) module CAS_interface : sig - (** Alternative interface, which may perform better on architectures without - FAD instructions (e.g. AArch). + (** Alternative interface, which may perform better on architectures without + FAD instructions (e.g. AArch). - CAS_interface should not be the default choice. It may be a little faster + CAS_interface should not be the default choice. It may be a little faster on ARM, but it is going to be a few times slower than standard on x86. *) diff --git a/src/mpsc_queue.mli b/src/mpsc_queue.mli index 34195201..bc7b3b32 100644 --- a/src/mpsc_queue.mli +++ b/src/mpsc_queue.mli @@ -1,5 +1,6 @@ -(** A lock-free multi-producer, single-consumer, thread-safe queue +(** Lock-free multi-producer, single-consumer, domain-safe queue without support for cancellation. + This makes a good data structure for a scheduler's run queue and is currently (September 2022) used for Eio's scheduler. *) @@ -9,26 +10,35 @@ type 'a t exception Closed val create : unit -> 'a t -(** [create ()] is a new empty queue. *) +(** [create ()] returns a new empty queue. *) val push : 'a t -> 'a -> unit -(** [push t x] adds [x] to the tail of the queue. - This can be used safely by multiple producer domains, in parallel with the other operations. - @raise Closed if [t] is closed. *) +(** [push q v] adds the element [v] at the end of the queue [q]. This + can be used safely by multiple producer domains, in parallel with + the other operations. -val push_head : 'a t -> 'a -> unit -(** [push_head t x] inserts [x] at the head of the queue. - This can only be used by the consumer (if run in parallel with {!pop}, the item might be skipped). - @raise Closed if [t] is closed and empty. *) + @raise Closed if [q] is closed. *) val pop : 'a t -> 'a option -(** [pop t] removes the head item from [t] and returns it. - Returns [None] if [t] is currently empty. - @raise Closed if [t] has been closed and is empty. *) +(** [pop q] removes and returns the first element in queue [q] or + returns [None] if the queue is empty. + + @raise Closed if [q] is closed and empty. *) + +val push_head : 'a t -> 'a -> unit +(** [push_head q v] adds the element [v] at the head of the queue + [q]. This can only be used by the consumer (if run in parallel + with {!pop}, the item might be skipped). + + @raise Closed if [q] is closed and empty. *) val is_empty : 'a t -> bool -(** [is_empty t] is [true] if calling [pop] would return [None]. - @raise Closed if [t] has been closed and is empty. *) +(** [is_empty q] is [true] if calling [pop] would return [None]. + + @raise Closed if [q] is closed and empty. *) val close : 'a t -> unit -(** [close t] marks [t] as closed, preventing any further items from being pushed. *) +(** [close q] marks [q] as closed, preventing any further items from + being pushed by the producers (i.e. with {!push}). + + @raise Closed if [q] has already been closed. *) diff --git a/src/lockfree.ml b/src/saturn.ml similarity index 85% rename from src/lockfree.ml rename to src/saturn.ml index 57eb3b9d..ca2e063a 100644 --- a/src/lockfree.ml +++ b/src/saturn.ml @@ -25,10 +25,11 @@ Copyright (c) 2017, Nicolas ASSOUAD ######## *) -module Ws_deque = Ws_deque -module Spsc_queue = Spsc_queue -module Mpsc_queue = Mpsc_queue -module Treiber_stack = Treiber_stack -module Michael_scott_queue = Michael_scott_queue + +module Queue = Michael_scott_queue +module Stack = Treiber_stack +module Work_stealing_deque = Ws_deque +module Single_prod_single_cons_queue = Spsc_queue +module Single_consumer_queue = Mpsc_queue +module Relaxed_queue = Mpmc_relaxed_queue module Backoff = Backoff -module Mpmc_relaxed_queue = Mpmc_relaxed_queue diff --git a/src/lockfree.mli b/src/saturn.mli similarity index 80% rename from src/lockfree.mli rename to src/saturn.mli index 5b50ca60..923254f5 100644 --- a/src/lockfree.mli +++ b/src/saturn.mli @@ -4,10 +4,6 @@ %%NAME%% %%VERSION%% ---------------------------------------------------------------------------*) -(** Lock-free data structures for Multicore OCaml *) - -(** {1 Lockfree} *) - (*--------------------------------------------------------------------------- Copyright (c) 2016 KC Sivaramakrishnan @@ -30,10 +26,17 @@ Copyright (c) 2017, Nicolas ASSOUAD ######## *) -module Ws_deque = Ws_deque -module Spsc_queue = Spsc_queue -module Mpsc_queue = Mpsc_queue -module Treiber_stack = Treiber_stack -module Michael_scott_queue = Michael_scott_queue -module Mpmc_relaxed_queue = Mpmc_relaxed_queue +(** Domain-safe data structures for Multicore OCaml *) + +(** {1 Data structures} *) + +module Queue = Michael_scott_queue +module Stack = Treiber_stack +module Work_stealing_deque = Ws_deque +module Single_prod_single_cons_queue = Spsc_queue +module Single_consumer_queue = Mpsc_queue +module Relaxed_queue = Mpmc_relaxed_queue + +(** {2 Other} *) + module Backoff = Backoff diff --git a/src/spsc_queue.mli b/src/spsc_queue.mli index 26ecd576..dc69b3a4 100644 --- a/src/spsc_queue.mli +++ b/src/spsc_queue.mli @@ -1,24 +1,29 @@ +(** Single producer single consumer queue. *) + type 'a t -(** Type of single-producer single-consumer non-resizable thread-safe +(** Type of single-producer single-consumer non-resizable domain-safe queue that works in FIFO order. *) exception Full +(** Raised when {!push} is applied to a full queue. *) val create : size_exponent:int -> 'a t -(** [create ~size_exponent:int] creates a empty queue of size - [2^size_exponent]. *) +(** [create ~size_exponent:int] returns a new queue of maximum size + [2^size_exponent] and initially empty. *) val push : 'a t -> 'a -> unit -(** [push q v] pushes [v] at the back of the queue. - +(** [push q v] adds the element [v] at the end of the queue [q]. This + method can be used by at most one domain at the time. + @raise [Full] if the queue is full. *) val pop : 'a t -> 'a option -(** [pop q] removes element from head of the queue, if any. This method can be used by - at most 1 thread at the time. *) +(** [pop q] removes and returns the first element in queue [q], or + returns [None] if the queue is empty. This method can be used by + at most one domain at the time. *) val size : 'a t -> int (** [size] returns the size of the queue. This method linearizes only when called - from either enqueuer or dequeuer thread. Otherwise, it is safe to call but + from either consumer or producer domain. Otherwise, it is safe to call but provides only an *indication* of the size of the structure. *) diff --git a/src/treiber_stack.mli b/src/treiber_stack.mli index 70968d90..6dc3644c 100644 --- a/src/treiber_stack.mli +++ b/src/treiber_stack.mli @@ -1,17 +1,20 @@ -(** Classic multi-producer multi-consumer Treiber stack. Robust and flexible. - Recommended starting point when needing LIFO structure. *) +(** Classic multi-producer multi-consumer Treiber stack. + + All function are lockfree. It is the recommended starting point + when needing LIFO structure. *) type 'a t (** Type of Treiber stack holding items of type [t]. *) val create : unit -> 'a t -(** [create] creates an empty Treiber stack. *) +(** [create ()] returns a new and empty Treiber stack. *) val is_empty : 'a t -> bool -(** [is_empty] checks whether stack is empty. *) +(** [is_empty s] checks whether stack [s] is empty. *) val push : 'a t -> 'a -> unit -(** [push] inserts element into the stack. *) +(** [push s v] adds the element [v] at the top of stack [s]. *) val pop : 'a t -> 'a option -(** [pop] removes the youngest element from the stack (if any). *) +(** [pop a] removes and returns the topmost element in the + stack [s], or returns [None] if the stack is empty. *) diff --git a/src/ws_deque.mli b/src/ws_deque.mli index e58e6cfc..ff1f2e09 100644 --- a/src/ws_deque.mli +++ b/src/ws_deque.mli @@ -1,16 +1,16 @@ -(** A lock-free single-producer, multi-consumer dynamic-size double-ended queue (deque). +(** Lock-free single-producer, multi-consumer dynamic-size double-ended queue (deque). The main strength of deque in a typical work-stealing setup with per-core structure - is efficient work distribution. Owner uses [push] and [pop] method to operate at - one end of the deque, while other (free) cores can efficiently steal work on the - other side. - - This approach is great for throughput. Stealers and owner working on different sides - reduces contention in work distribution. Further, local LIFO order runs related tasks - one after one improves locality. - - On the other hand, the local LIFO order does not offer any fairness guarantees. - Thus, it is not the best choice when tail latency matters. + is efficient work distribution. Owner uses [push] and [pop] method to operate at + one end of the deque, while other (free) cores can efficiently steal work on the + other side. + + This approach is great for throughput. Stealers and owner working on different sides + reduces contention in work distribution. Further, local LIFO order runs related tasks + one after one improves locality. + + On the other hand, the local LIFO order does not offer any fairness guarantees. + Thus, it is not the best choice when tail latency matters. *) module type S = sig @@ -18,22 +18,28 @@ module type S = sig (** Type of work-stealing queue *) val create : unit -> 'a t - (** Returns a fresh empty work-stealing queue *) + (** [create ()] returns a new empty work-stealing queue. *) + + (** {1 Queue owner functions} *) val push : 'a t -> 'a -> unit - (** [push q v] pushes [v] to the front of the queue. + (** [push t v] adds [v] to the front of the queue [q]. It should only be invoked by the domain which owns the queue [q]. *) val pop : 'a t -> 'a - (** [pop q] removes an element [e] from the front of the queue and returns - it. It should only be invoked by the domain which owns the queue [q]. + (** [pop q] removes and returns the first element in queue + [q].It should only be invoked by the domain which owns the queue + [q]. @raise [Exit] if the queue is empty. *) + (** {1 Stealers function} *) + val steal : 'a t -> 'a - (** [steal q] removes an element from the back of the queue and returns - it. It should only be invoked by domain which doesn't own the queue [q]. + (** [steal q] removes and returns the last element from queue + [q]. It should only be invoked by domain which doesn't own the + queue [q]. @raise [Exit] if the queue is empty. *) diff --git a/test/README.md b/test/README.md index 9536cbde..ae253e22 100644 --- a/test/README.md +++ b/test/README.md @@ -1,10 +1,67 @@ -## About dscheck tests +### Introduction -Dscheck tests need to use dscheck `TracedAtomic` library, which adds effects to `Stdlib.Atomic` to track calls to atomic functions. To make it work : -- the `Atomic` standard library is shadowed by [`Dscheck.TracedAtomic`](atomic/atomic.ml) -- every datastructure implementation is copied in its respective tests directory. The copied version is used only for dscheck tests and is compiled with the `shadowing` atomic library +Several kind of tests are provided for each data structure: + +- unitary tests and `qcheck` tests: check semantics and expected behaviors with + one and more domains; +- `STM` tests: also check semantics as well as _linearizability_ for two domains + (see + [multicoretests library](https://github.com/ocaml-multicore/multicoretests)); +- `dscheck` (for lockfree data structures): checks lock-freedom for as many + domains as wanted (for two domains most of the time). It is limited to the + paths explored by the tests. + +### Unitary parallel tests and `QCheck` tests + +Every data structure should have separate parallel tests for all core operations +and for most useful combinations of them to make sure things work the way you +expected them to, even in parallel. + +Inside the parallel tests, it's important to ensure there's a high chance of +actual parallel execution. Keep in mind that spawning a domain is an expensive +operation: if a domain only launches a few simple operations, it will most +likely run in isolation. Here are a few tricks to ensure your tests actually +runs with parallelism: + +- make a domain repeat its operations. In particular, that usually works well + when testing a single function. +- use a semaphore to make all domains wait for each other before starting (see + [these tests for example) ](ws_deque/qcheck_ws_deque.ml)). +- if you are still not sure your tests have a good chance to run in parallel, + try it in the top level, and use print or outputs to understand what is + happening. + +### Linearizability test with `STM` (see [multicoretests](https://github.com/ocaml-multicore/multicoretests)) + +#### How to write `STM` tests ? + +`STM` tests work by comparing the results of two domains each executing a random +list of method calls to a sequential model provided by the user. Most of the +time, these tests are easy and quick to write and can catch a lot of bugs. + +If all domains can use every functions of the tested data structure, you can +have a look to +[stm test for Treiber's stack](treiber_stack/stm_treiber_stack.ml). If domains +have specific roles (producer/consumer/stealer etc..), +[this one](ws_deque/stm_ws_deque.ml) is for a work-stealing deque and is a +better example. + +### Lock-free property with [`dscheck`](https://github.com/ocaml-multicore/dscheck). + +`dscheck` is a model checker. Each provided test is run multiple times, each +time exploring a different interleaving between atomic operations. This checks +that there is no `blocking` paths in the ones explored by these tests (if a +trace is blocking, the test does not end) + +#### How is `Atomic` library shadowed ? + +Dscheck tests need to use dscheck `TracedAtomic` library, which adds effects to +`Stdlib.Atomic` to track calls to atomic functions. To make it work, every +datastructure implementation is copied in its respective tests directory and +compiled using the `dscheck` [atomic library](atomic/atomic.ml). For example, in [ws_deque/dune](ws_deque/dune) : + ``` ; Copy implementation file and its dependencies (rule @@ -19,4 +76,12 @@ For example, in [ws_deque/dune](ws_deque/dune) : (libraries atomic dscheck alcotest) (modules ArrayExtra ws_deque ws_deque_dscheck)) ``` -Dscheck test rule does not require `lockfree` but require `atomic` which is the shadowed atomic library. + +We can see that `dscheck` test compilation does not depend on `lockfree` (since +the data structure code is copy-paste in the test directory) but require +`atomic` which is the shadowing atomic library. + +#### What about other progress properties ? + +Right now, `dscheck` only checks for lock-freedom. In a near future, it should +also be able to deal with lock and checks for deadlock-freedom. diff --git a/test/michael_scott_queue/dune b/test/michael_scott_queue/dune index e89e28db..11fca835 100644 --- a/test/michael_scott_queue/dune +++ b/test/michael_scott_queue/dune @@ -11,12 +11,12 @@ (test (name qcheck_michael_scott_queue) - (libraries lockfree qcheck qcheck-alcotest) + (libraries saturn qcheck qcheck-alcotest) (modules qcheck_michael_scott_queue)) (test (name stm_michael_scott_queue) (modules stm_michael_scott_queue) - (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (libraries saturn qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/michael_scott_queue/qcheck_michael_scott_queue.ml b/test/michael_scott_queue/qcheck_michael_scott_queue.ml index d11ab069..70a4cd55 100644 --- a/test/michael_scott_queue/qcheck_michael_scott_queue.ml +++ b/test/michael_scott_queue/qcheck_michael_scott_queue.ml @@ -1,4 +1,4 @@ -open Lockfree +open Saturn.Queue let tests_sequential = QCheck. @@ -7,39 +7,37 @@ let tests_sequential = Test.make ~name:"push" (list int) (fun lpush -> assume (lpush <> []); (* Building a random queue *) - let queue = Michael_scott_queue.create () in - List.iter (Michael_scott_queue.push queue) lpush; + let queue = create () in + List.iter (push queue) lpush; (* Testing property *) - not (Michael_scott_queue.is_empty queue)); + not (is_empty queue)); (* TEST 2 - push, pop until empty *) Test.make ~name:"push_pop_until_empty" (list int) (fun lpush -> (* Building a random queue *) - let queue = Michael_scott_queue.create () in - List.iter (Michael_scott_queue.push queue) lpush; + let queue = create () in + List.iter (push queue) lpush; (* Popping until [is_empty q] is true *) let count = ref 0 in - while not (Michael_scott_queue.is_empty queue) do + while not (is_empty queue) do incr count; - ignore (Michael_scott_queue.pop queue) + ignore (pop queue) done; (* Testing property *) - Michael_scott_queue.pop queue = None && !count = List.length lpush); + pop queue = None && !count = List.length lpush); (* TEST 3 - push, pop, check FIFO *) Test.make ~name:"fifo" (list int) (fun lpush -> (* Building a random queue *) - let queue = Michael_scott_queue.create () in - List.iter (Michael_scott_queue.push queue) lpush; + let queue = create () in + List.iter (push queue) lpush; let out = ref [] in let insert v = out := v :: !out in for _ = 1 to List.length lpush do - match Michael_scott_queue.pop queue with - | None -> assert false - | Some v -> insert v + match pop queue with None -> assert false | Some v -> insert v done; (* Testing property *) @@ -53,12 +51,11 @@ let tests_one_consumer_one_producer = Parallel [push] and [pop]. *) Test.make ~count:10_000 ~name:"parallel_fifo" (list int) (fun lpush -> (* Initialization *) - let queue = Michael_scott_queue.create () in + let queue = create () in (* Producer pushes. *) let producer = - Domain.spawn (fun () -> - List.iter (Michael_scott_queue.push queue) lpush) + Domain.spawn (fun () -> List.iter (push queue) lpush) in let fifo = @@ -66,12 +63,12 @@ let tests_one_consumer_one_producer = (fun acc item -> let popped = ref None in while Option.is_none !popped do - popped := Michael_scott_queue.pop queue + popped := pop queue done; acc && item = Option.get !popped) true lpush in - let empty = Michael_scott_queue.is_empty queue in + let empty = is_empty queue in (* Ensure nothing is left behind. *) Domain.join producer; @@ -87,7 +84,7 @@ let tests_two_domains = Test.make ~count:10_000 ~name:"parallel_pop_push" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let queue = Michael_scott_queue.create () in + let queue = create () in let sema = Semaphore.Binary.make false in (* Using these lists instead of a random one enables to @@ -98,9 +95,9 @@ let tests_two_domains = let work lpush = List.map (fun elt -> - Michael_scott_queue.push queue elt; + push queue elt; Domain.cpu_relax (); - Michael_scott_queue.pop queue) + pop queue) lpush in @@ -147,7 +144,7 @@ let tests_two_domains = Test.make ~count:10_000 ~name:"parallel_pop_push_random" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let queue = Michael_scott_queue.create () in + let queue = create () in let sema = Semaphore.Binary.make false in let lpush1 = List.init npush1 (fun i -> i) in @@ -164,11 +161,11 @@ let tests_two_domains = match lpush with | [] -> popped | elt :: xs -> - Michael_scott_queue.push queue elt; + push queue elt; loop xs popped) else ( incr consecutive_pop; - let p = Michael_scott_queue.pop queue in + let p = pop queue in loop lpush (p :: popped)) in loop lpush [] @@ -200,7 +197,7 @@ let tests_two_domains = (* Pop everything that is still on the queue *) let popped3 = let rec loop popped = - match Michael_scott_queue.pop queue with + match pop queue with | None -> popped | Some v -> loop (v :: popped) in diff --git a/test/michael_scott_queue/stm_michael_scott_queue.ml b/test/michael_scott_queue/stm_michael_scott_queue.ml index a2c7ffaf..e36a464b 100644 --- a/test/michael_scott_queue/stm_michael_scott_queue.ml +++ b/test/michael_scott_queue/stm_michael_scott_queue.ml @@ -2,7 +2,7 @@ open QCheck open STM -module Ms_queue = Lockfree.Michael_scott_queue +module Ms_queue = Saturn.Queue module MSQConf = struct type cmd = Push of int | Pop | Is_empty @@ -61,7 +61,7 @@ let () = QCheck_base_runner.run_tests_main [ MSQ_seq.agree_test ~count - ~name:"STM Lockfree.Michael_scott_queue test sequential"; + ~name:"STM Saturn.Michael_scott_queue test sequential"; MSQ_dom.agree_test_par ~count - ~name:"STM Lockfree.Michael_scott_queue test parallel"; + ~name:"STM Saturn.Michael_scott_queue test parallel"; ] diff --git a/test/mpmc_relaxed_queue/dune b/test/mpmc_relaxed_queue/dune index 5c6df1e6..38e60931 100644 --- a/test/mpmc_relaxed_queue/dune +++ b/test/mpmc_relaxed_queue/dune @@ -1,4 +1,4 @@ (test (name test_mpmc_relaxed_queue) - (libraries lockfree unix alcotest) + (libraries saturn unix alcotest) (modules test_mpmc_relaxed_queue)) diff --git a/test/mpmc_relaxed_queue/test_mpmc_relaxed_queue.ml b/test/mpmc_relaxed_queue/test_mpmc_relaxed_queue.ml index 99f7a820..106b97e8 100644 --- a/test/mpmc_relaxed_queue/test_mpmc_relaxed_queue.ml +++ b/test/mpmc_relaxed_queue/test_mpmc_relaxed_queue.ml @@ -1,14 +1,14 @@ -open Lockfree +open Saturn let smoke_test (push, pop) () = - let queue = Mpmc_relaxed_queue.create ~size_exponent:2 () in + let queue = Relaxed_queue.create ~size_exponent:2 () in (* enqueue 4 *) for i = 1 to 4 do Alcotest.(check bool) "there should be space in the queue" (push queue i) true done; assert (not (push queue 0)); - let ({ tail; head; _ } : 'a Mpmc_relaxed_queue.t) = queue in + let ({ tail; head; _ } : 'a Relaxed_queue.t) = queue in assert (Atomic.get tail = 4); assert (Atomic.get head = 0); (* dequeue 4 *) @@ -19,7 +19,7 @@ let smoke_test (push, pop) () = Alcotest.(check (option int)) "queue should be empty" None (pop queue) let two_threads_test (push, pop) () = - let queue = Mpmc_relaxed_queue.create ~size_exponent:2 () in + let queue = Relaxed_queue.create ~size_exponent:2 () in let num_of_elements = 1_000_000 in (* start dequeuer *) let dequeuer = @@ -58,19 +58,18 @@ let taker wfo queue num_of_elements () = Wait_for_others.wait wfo; let i = ref 0 in while !i < num_of_elements do - if Option.is_some (Mpmc_relaxed_queue.Not_lockfree.pop queue) then - i := !i + 1 + if Option.is_some (Relaxed_queue.Not_lockfree.pop queue) then i := !i + 1 done let pusher wfo queue num_of_elements () = Wait_for_others.wait wfo; let i = ref 0 in while !i < num_of_elements do - if Mpmc_relaxed_queue.Not_lockfree.push queue !i then i := !i + 1 + if Relaxed_queue.Not_lockfree.push queue !i then i := !i + 1 done let run_test num_takers num_pushers () = - let queue = Mpmc_relaxed_queue.create ~size_exponent:3 () in + let queue = Relaxed_queue.create ~size_exponent:3 () in let num_of_elements = 4_000_000 in let wfo = Wait_for_others.init ~total_expected:(num_takers + num_pushers) in let _ = @@ -88,7 +87,7 @@ let run_test num_takers num_pushers () = in Sys.opaque_identity (List.map Domain.join (pushers @ takers)) in - let ({ array; head; tail; _ } : 'a Mpmc_relaxed_queue.t) = queue in + let ({ array; head; tail; _ } : 'a Relaxed_queue.t) = queue in let head_val = Atomic.get head in let tail_val = Atomic.get tail in Alcotest.(check int) "hd an tl match" head_val tail_val; @@ -99,38 +98,38 @@ let run_test num_takers num_pushers () = array let smoke_test_spinning () = - let queue = Mpmc_relaxed_queue.create ~size_exponent:2 () in + let queue = Relaxed_queue.create ~size_exponent:2 () in (* enqueue 4 *) for i = 1 to 4 do - Mpmc_relaxed_queue.Spin.push queue i + Relaxed_queue.Spin.push queue i done; - assert (not (Mpmc_relaxed_queue.Not_lockfree.push queue 0)); - let ({ tail; head; _ } : 'a Mpmc_relaxed_queue.t) = queue in + assert (not (Relaxed_queue.Not_lockfree.push queue 0)); + let ({ tail; head; _ } : 'a Relaxed_queue.t) = queue in assert (Atomic.get tail = 4); assert (Atomic.get head = 0); (* dequeue 4 *) for i = 1 to 4 do Alcotest.(check (option int)) "items should come out in FIFO order" (Some i) - (Mpmc_relaxed_queue.Not_lockfree.pop queue) + (Relaxed_queue.Not_lockfree.pop queue) done; Alcotest.(check (option int)) "queue should be empty" None - (Mpmc_relaxed_queue.Not_lockfree.pop queue) + (Relaxed_queue.Not_lockfree.pop queue) let two_threads_spin_test () = - let queue = Mpmc_relaxed_queue.create ~size_exponent:2 () in + let queue = Relaxed_queue.create ~size_exponent:2 () in let num_of_elements = 1_000_000 in (* start dequeuer *) let dequeuer = Domain.spawn (fun () -> for i = 1 to num_of_elements do - assert (Mpmc_relaxed_queue.Spin.pop queue == i) + assert (Relaxed_queue.Spin.pop queue == i) done) in (* enqueue *) for i = 1 to num_of_elements do - Mpmc_relaxed_queue.Spin.push queue i + Relaxed_queue.Spin.push queue i done; Domain.join dequeuer |> ignore; () @@ -138,30 +137,32 @@ let two_threads_spin_test () = let () = let open Alcotest in run "Mpmc_queue" - (let open Mpmc_relaxed_queue.Not_lockfree in - [ - ( "single-thread", - [ test_case "is it a queue" `Quick (smoke_test (push, pop)) ] ); - ( "validate items", - [ test_case "1 prod. 1 cons." `Quick (two_threads_test (push, pop)) ] ); - ( "validate indices under load", - [ - test_case " 4 prod. 4 cons." `Slow (run_test 4 4); - test_case " 8 prod. 1 cons." `Slow (run_test 8 1); - test_case " 1 prod. 8 cons." `Slow (run_test 1 8); - ] ); - ] - @ - let open Mpmc_relaxed_queue.Not_lockfree.CAS_interface in - [ - ( "single-thread-CAS-intf", - [ test_case "is it a queue" `Quick (smoke_test (push, pop)) ] ); - ( "validate items-CAS-intf", - [ test_case "1 prod. 1 cons." `Quick (two_threads_test (push, pop)) ] ); - ] - @ [ - ( "single-thread-spinning", - [ test_case "is it a queue" `Quick smoke_test_spinning ] ); - ( "validate-items-spinning", - [ test_case "1 prod. 1 cons" `Quick two_threads_spin_test ] ); - ]) + (let open Relaxed_queue.Not_lockfree in + [ + ( "single-thread", + [ test_case "is it a queue" `Quick (smoke_test (push, pop)) ] ); + ( "validate items", + [ test_case "1 prod. 1 cons." `Quick (two_threads_test (push, pop)) ] + ); + ( "validate indices under load", + [ + test_case " 4 prod. 4 cons." `Slow (run_test 4 4); + test_case " 8 prod. 1 cons." `Slow (run_test 8 1); + test_case " 1 prod. 8 cons." `Slow (run_test 1 8); + ] ); + ] + @ + let open Relaxed_queue.Not_lockfree.CAS_interface in + [ + ( "single-thread-CAS-intf", + [ test_case "is it a queue" `Quick (smoke_test (push, pop)) ] ); + ( "validate items-CAS-intf", + [ test_case "1 prod. 1 cons." `Quick (two_threads_test (push, pop)) ] + ); + ] + @ [ + ( "single-thread-spinning", + [ test_case "is it a queue" `Quick smoke_test_spinning ] ); + ( "validate-items-spinning", + [ test_case "1 prod. 1 cons" `Quick two_threads_spin_test ] ); + ]) diff --git a/test/mpsc_queue/dune b/test/mpsc_queue/dune index 9776efd6..df8412aa 100644 --- a/test/mpsc_queue/dune +++ b/test/mpsc_queue/dune @@ -8,12 +8,12 @@ (test (name qcheck_mpsc_queue) - (libraries lockfree qcheck qcheck-alcotest) + (libraries saturn qcheck qcheck-alcotest) (modules qcheck_mpsc_queue)) (test (name stm_mpsc_queue) (modules stm_mpsc_queue) - (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (libraries saturn qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/mpsc_queue/qcheck_mpsc_queue.ml b/test/mpsc_queue/qcheck_mpsc_queue.ml index f8e0d4e3..0484e174 100644 --- a/test/mpsc_queue/qcheck_mpsc_queue.ml +++ b/test/mpsc_queue/qcheck_mpsc_queue.ml @@ -1,4 +1,4 @@ -module Mpsc_queue = Lockfree.Mpsc_queue +module Mpsc_queue = Saturn.Single_consumer_queue (* Mpsc_queue is a multiple producers, single consumer queue. *) (* Producers can use the functions diff --git a/test/mpsc_queue/stm_mpsc_queue.ml b/test/mpsc_queue/stm_mpsc_queue.ml index 83ecb40d..f8e17344 100644 --- a/test/mpsc_queue/stm_mpsc_queue.ml +++ b/test/mpsc_queue/stm_mpsc_queue.ml @@ -3,7 +3,7 @@ open QCheck open STM open Util -module Mpsc_queue = Lockfree.Mpsc_queue +module Mpsc_queue = Saturn.Single_consumer_queue module MPSCConf = struct type cmd = Push of int | Pop | Push_head of int | Is_empty | Close @@ -105,8 +105,8 @@ let () = let count = 1000 in QCheck_base_runner.run_tests_main [ - MPSC_seq.agree_test ~count ~name:"STM Lockfree.Mpsc_queue test sequential"; - agree_test_par_asym ~count ~name:"STM Lockfree.Mpsc_queue test parallel"; + MPSC_seq.agree_test ~count ~name:"STM Saturn.Mpsc_queue test sequential"; + agree_test_par_asym ~count ~name:"STM Saturn.Mpsc_queue test parallel"; MPSC_dom.neg_agree_test_par ~count - ~name:"STM Lockfree.Mpsc_queue test parallel, negative"; + ~name:"STM Saturn.Mpsc_queue test parallel, negative"; ] diff --git a/test/spsc_queue/dune b/test/spsc_queue/dune index 9bf002b1..0b14b4c3 100644 --- a/test/spsc_queue/dune +++ b/test/spsc_queue/dune @@ -8,17 +8,17 @@ (test (name test_spsc_queue) - (libraries lockfree) + (libraries saturn) (modules test_spsc_queue)) (test (name qcheck_spsc_queue) - (libraries lockfree qcheck "qcheck-alcotest") + (libraries saturn qcheck "qcheck-alcotest") (modules qcheck_spsc_queue)) (test (name stm_spsc_queue) (modules stm_spsc_queue) - (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (libraries saturn qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/spsc_queue/qcheck_spsc_queue.ml b/test/spsc_queue/qcheck_spsc_queue.ml index 344f743e..e3050468 100644 --- a/test/spsc_queue/qcheck_spsc_queue.ml +++ b/test/spsc_queue/qcheck_spsc_queue.ml @@ -1,4 +1,4 @@ -module Spsc_queue = Lockfree.Spsc_queue +module Spsc_queue = Saturn.Single_prod_single_cons_queue let keep_some l = List.filter Option.is_some l |> List.map Option.get let keep_n_first n = List.filteri (fun i _ -> i < n) diff --git a/test/spsc_queue/stm_spsc_queue.ml b/test/spsc_queue/stm_spsc_queue.ml index d8d01c51..d581872d 100644 --- a/test/spsc_queue/stm_spsc_queue.ml +++ b/test/spsc_queue/stm_spsc_queue.ml @@ -3,7 +3,7 @@ open QCheck open STM open Util -module Spsc_queue = Lockfree.Spsc_queue +module Spsc_queue = Saturn.Single_prod_single_cons_queue module SPSCConf = struct type cmd = Push of int | Pop @@ -79,9 +79,9 @@ let () = let count = 1000 in QCheck_base_runner.run_tests_main [ - SPSC_seq.agree_test ~count ~name:"STM Lockfree.Spsc_queue test sequential"; - agree_test_par_asym ~count ~name:"STM Lockfree.Spsc_queue test parallel"; + SPSC_seq.agree_test ~count ~name:"STM Saturn.Spsc_queue test sequential"; + agree_test_par_asym ~count ~name:"STM Saturn.Spsc_queue test parallel"; (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) SPSC_dom.neg_agree_test_par ~count - ~name:"STM Lockfree.Spsc_queue test parallel, negative"; + ~name:"STM Saturn.Spsc_queue test parallel, negative"; ] diff --git a/test/spsc_queue/test_spsc_queue.ml b/test/spsc_queue/test_spsc_queue.ml index ac6b4d67..e2c9d481 100644 --- a/test/spsc_queue/test_spsc_queue.ml +++ b/test/spsc_queue/test_spsc_queue.ml @@ -1,4 +1,4 @@ -open Lockfree +module Spsc_queue = Saturn.Single_prod_single_cons_queue (** Tests *) let test_empty () = diff --git a/test/treiber_stack/dune b/test/treiber_stack/dune index 841cf9eb..22cbcf84 100644 --- a/test/treiber_stack/dune +++ b/test/treiber_stack/dune @@ -11,12 +11,12 @@ (test (name qcheck_treiber_stack) - (libraries lockfree qcheck qcheck-alcotest) + (libraries saturn qcheck qcheck-alcotest) (modules qcheck_treiber_stack)) (test (name stm_treiber_stack) (modules stm_treiber_stack) - (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (libraries saturn qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/treiber_stack/qcheck_treiber_stack.ml b/test/treiber_stack/qcheck_treiber_stack.ml index d33f6d60..eced6fdc 100644 --- a/test/treiber_stack/qcheck_treiber_stack.ml +++ b/test/treiber_stack/qcheck_treiber_stack.ml @@ -1,4 +1,4 @@ -open Lockfree +open Saturn.Stack let tests_sequential = QCheck. @@ -7,39 +7,37 @@ let tests_sequential = Test.make ~name:"push" (list int) (fun lpush -> assume (lpush <> []); (* Building a random stack *) - let stack = Treiber_stack.create () in - List.iter (Treiber_stack.push stack) lpush; + let stack = create () in + List.iter (push stack) lpush; (* Testing property *) - not (Treiber_stack.is_empty stack)); + not (is_empty stack)); (* TEST 2 - push, pop until empty *) Test.make ~name:"push_pop_until_empty" (list int) (fun lpush -> (* Building a random stack *) - let stack = Treiber_stack.create () in - List.iter (Treiber_stack.push stack) lpush; + let stack = create () in + List.iter (push stack) lpush; (* Popping until [is_empty q] is true *) let count = ref 0 in - while not (Treiber_stack.is_empty stack) do + while not (is_empty stack) do incr count; - ignore (Treiber_stack.pop stack) + ignore (pop stack) done; (* Testing property *) - Treiber_stack.pop stack = None && !count = List.length lpush); + pop stack = None && !count = List.length lpush); (* TEST 3 - push, pop, check LIFO *) Test.make ~name:"lifo" (list int) (fun lpush -> (* Building a random stack *) - let stack = Treiber_stack.create () in - List.iter (Treiber_stack.push stack) lpush; + let stack = create () in + List.iter (push stack) lpush; let out = ref [] in let insert v = out := v :: !out in for _ = 1 to List.length lpush do - match Treiber_stack.pop stack with - | None -> assert false - | Some v -> insert v + match pop stack with None -> assert false | Some v -> insert v done; Printf.printf "------\n"; @@ -59,28 +57,28 @@ let tests_one_consumer_one_producer = Parallel [push] and [pop]. *) Test.make ~count:10_000 ~name:"parallel" (list int) (fun lpush -> (* Initialization *) - let stack = Treiber_stack.create () in + let stack = create () in let sema = Semaphore.Binary.make false in (* Producer pushes. *) let producer = Domain.spawn (fun () -> Semaphore.Binary.release sema; - List.iter (Treiber_stack.push stack) lpush) + List.iter (push stack) lpush) in while not (Semaphore.Binary.try_acquire sema) do Domain.cpu_relax () done; for _ = 1 to List.length lpush do - while Option.is_none (Treiber_stack.pop stack) do + while Option.is_none (pop stack) do () done done; (* Ensure nothing is left behind. *) Domain.join producer; - Treiber_stack.is_empty stack); + is_empty stack); ] let tests_two_domains = @@ -92,7 +90,7 @@ let tests_two_domains = Test.make ~count:10_000 ~name:"parallel_pop_push" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let stack = Treiber_stack.create () in + let stack = create () in let sema = Semaphore.Binary.make false in let lpush1 = List.init npush1 (fun i -> i) in @@ -101,9 +99,9 @@ let tests_two_domains = let work lpush = List.map (fun elt -> - Treiber_stack.push stack elt; + push stack elt; Domain.cpu_relax (); - Treiber_stack.pop stack) + pop stack) lpush in @@ -141,7 +139,7 @@ let tests_two_domains = Test.make ~count:10_000 ~name:"parallel_pop_push_random" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let stack = Treiber_stack.create () in + let stack = create () in let lpush1 = List.init npush1 (fun i -> i) in let lpush2 = List.init npush2 (fun i -> i + npush1) in @@ -158,11 +156,11 @@ let tests_two_domains = match lpush with | [] -> popped | elt :: xs -> - Treiber_stack.push stack elt; + push stack elt; loop xs popped) else ( incr consecutive_pop; - let p = Treiber_stack.pop stack in + let p = pop stack in loop lpush (p :: popped)) in loop lpush [] @@ -194,7 +192,7 @@ let tests_two_domains = (* Pop everything that is still on the queue *) let popped3 = let rec loop popped = - match Treiber_stack.pop stack with + match pop stack with | None -> popped | Some v -> loop (v :: popped) in diff --git a/test/treiber_stack/stm_treiber_stack.ml b/test/treiber_stack/stm_treiber_stack.ml index 2a4a5b1f..b02bdcef 100644 --- a/test/treiber_stack/stm_treiber_stack.ml +++ b/test/treiber_stack/stm_treiber_stack.ml @@ -2,7 +2,7 @@ open QCheck open STM -module Treiber_stack = Lockfree.Treiber_stack +module Treiber_stack = Saturn.Stack module TSConf = struct type cmd = Push of int | Pop | Is_empty @@ -60,8 +60,7 @@ let () = let count = 500 in QCheck_base_runner.run_tests_main [ - TS_seq.agree_test ~count - ~name:"STM Lockfree.Treiber_stack test sequential"; + TS_seq.agree_test ~count ~name:"STM Saturn.Treiber_stack test sequential"; TS_dom.agree_test_par ~count - ~name:"STM Lockfree.Treiber_stack test parallel"; + ~name:"STM Saturn.Treiber_stack test parallel"; ] diff --git a/test/ws_deque/dune b/test/ws_deque/dune index 68f334c5..06515680 100644 --- a/test/ws_deque/dune +++ b/test/ws_deque/dune @@ -11,17 +11,17 @@ (test (name test_ws_deque) - (libraries lockfree) + (libraries saturn) (modules test_ws_deque)) (test (name qcheck_ws_deque) - (libraries lockfree qcheck "qcheck-alcotest") + (libraries saturn qcheck "qcheck-alcotest") (modules qcheck_ws_deque)) (test (name stm_ws_deque) (modules stm_ws_deque) - (libraries lockfree qcheck-stm.sequential qcheck-stm.domain) + (libraries saturn qcheck-stm.sequential qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/ws_deque/qcheck_ws_deque.ml b/test/ws_deque/qcheck_ws_deque.ml index c1ac9255..2cf27e03 100644 --- a/test/ws_deque/qcheck_ws_deque.ml +++ b/test/ws_deque/qcheck_ws_deque.ml @@ -1,4 +1,4 @@ -module Ws_deque = Lockfree.Ws_deque.M +module Ws_deque = Saturn.Work_stealing_deque.M (* Sequential building of a deque *) let deque_of_list l = diff --git a/test/ws_deque/stm_ws_deque.ml b/test/ws_deque/stm_ws_deque.ml index 4eb91c7e..8a517344 100644 --- a/test/ws_deque/stm_ws_deque.ml +++ b/test/ws_deque/stm_ws_deque.ml @@ -3,7 +3,7 @@ open QCheck open STM open Util -module Ws_deque = Lockfree.Ws_deque +module Ws_deque = Saturn.Work_stealing_deque module WSDConf = struct type cmd = Push of int | Pop | Steal @@ -78,9 +78,9 @@ let () = let count = 1000 in QCheck_base_runner.run_tests_main [ - WSDT_seq.agree_test ~count ~name:"STM Lockfree.Ws_deque test sequential"; - agree_test_par_asym ~count ~name:"STM Lockfree.Ws_deque test parallel"; + WSDT_seq.agree_test ~count ~name:"STM Saturn.Ws_deque test sequential"; + agree_test_par_asym ~count ~name:"STM Saturn.Ws_deque test parallel"; (* Note: this can generate, e.g., pop commands/actions in different threads, thus violating the spec. *) WSDT_dom.neg_agree_test_par ~count - ~name:"STM Lockfree.Ws_deque test parallel, negative"; + ~name:"STM Saturn.Ws_deque test parallel, negative"; ] diff --git a/test/ws_deque/test_ws_deque.ml b/test/ws_deque/test_ws_deque.ml index aa0dee0e..3f998dde 100644 --- a/test/ws_deque/test_ws_deque.ml +++ b/test/ws_deque/test_ws_deque.ml @@ -1,4 +1,4 @@ -open Lockfree.Ws_deque.M +open Saturn.Work_stealing_deque.M (** Tests *) let test_empty () = From 67164e56b97999494ef6a06cd2805d5b0935bb7e Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 4 Jul 2023 17:48:33 +0200 Subject: [PATCH 15/22] Refactor to separate lockfree from non-lockfree data structures. --- CHANGES.md | 2 +- README.md | 33 +++-- dune-project | 6 + saturn.opam | 2 +- saturn_lockfree.opam | 24 ++++ src/dune | 2 +- src/mpmc_relaxed_queue.ml | 136 +----------------- src/mpmc_relaxed_queue.mli | 2 +- src/saturn.ml | 12 +- src/saturn.mli | 13 +- {src => src_lockfree}/ArrayExtra.ml | 0 {src => src_lockfree}/backoff.ml | 0 {src => src_lockfree}/backoff.mli | 0 src_lockfree/dune | 4 + src_lockfree/lockfree.ml | 35 +++++ src_lockfree/lockfree.mli | 42 ++++++ {src => src_lockfree}/michael_scott_queue.ml | 0 {src => src_lockfree}/michael_scott_queue.mli | 0 src_lockfree/mpmc_relaxed_queue.ml | 134 +++++++++++++++++ src_lockfree/mpmc_relaxed_queue.mli | 36 +++++ {src => src_lockfree}/mpsc_queue.ml | 0 {src => src_lockfree}/mpsc_queue.mli | 0 {src => src_lockfree}/spsc_queue.ml | 0 {src => src_lockfree}/spsc_queue.mli | 0 {src => src_lockfree}/treiber_stack.ml | 0 {src => src_lockfree}/treiber_stack.mli | 0 {src => src_lockfree}/ws_deque.ml | 0 {src => src_lockfree}/ws_deque.mli | 0 test/michael_scott_queue/dune | 4 +- test/mpsc_queue/dune | 2 +- {seqtest => test/seqtest}/.gitignore | 0 {seqtest => test/seqtest}/Makefile | 0 {seqtest => test/seqtest}/Makefile.monolith | 0 {seqtest => test/seqtest}/README.md | 0 {seqtest => test/seqtest}/dune | 0 {seqtest => test/seqtest}/seqtest.ml | 0 test/spsc_queue/dune | 2 +- test/treiber_stack/dune | 4 +- test/ws_deque/dune | 4 +- 39 files changed, 330 insertions(+), 169 deletions(-) create mode 100644 saturn_lockfree.opam rename {src => src_lockfree}/ArrayExtra.ml (100%) rename {src => src_lockfree}/backoff.ml (100%) rename {src => src_lockfree}/backoff.mli (100%) create mode 100644 src_lockfree/dune create mode 100644 src_lockfree/lockfree.ml create mode 100644 src_lockfree/lockfree.mli rename {src => src_lockfree}/michael_scott_queue.ml (100%) rename {src => src_lockfree}/michael_scott_queue.mli (100%) create mode 100644 src_lockfree/mpmc_relaxed_queue.ml create mode 100644 src_lockfree/mpmc_relaxed_queue.mli rename {src => src_lockfree}/mpsc_queue.ml (100%) rename {src => src_lockfree}/mpsc_queue.mli (100%) rename {src => src_lockfree}/spsc_queue.ml (100%) rename {src => src_lockfree}/spsc_queue.mli (100%) rename {src => src_lockfree}/treiber_stack.ml (100%) rename {src => src_lockfree}/treiber_stack.mli (100%) rename {src => src_lockfree}/ws_deque.ml (100%) rename {src => src_lockfree}/ws_deque.mli (100%) rename {seqtest => test/seqtest}/.gitignore (100%) rename {seqtest => test/seqtest}/Makefile (100%) rename {seqtest => test/seqtest}/Makefile.monolith (100%) rename {seqtest => test/seqtest}/README.md (100%) rename {seqtest => test/seqtest}/dune (100%) rename {seqtest => test/seqtest}/seqtest.ml (100%) diff --git a/CHANGES.md b/CHANGES.md index 0480fabb..f3349e4a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,7 +4,7 @@ All notable changes to this project will be documented in this file. ## Not released -- Rename data structures and package, add docs (@lyrm) +- Add docs and rename/refactor to add a lockfree package (@lyrm) - Add STM tests for current data structures (@lyrm, @jmid) ## 0.3.1 diff --git a/README.md b/README.md index 2ad2ef6b..a0bda16f 100644 --- a/README.md +++ b/README.md @@ -2,24 +2,31 @@ --- -A collection of parallelism-safe data structures for OCaml 5. It contains: +This repository is a collection of parallelism-safe data structures for OCaml 5. +They are contained in two packages: -| Name | What is it ? | Sources | -| -------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -| [Treiber Stack](src/treiber_stack.mli) | A classic multi-producer multi-consumer stack, robust and flexible. Recommended starting point when needing LIFO structure | | -| [Michael-Scott Queue](src/michael_scott_queue.mli) | A classic multi-producer multi-consumer queue, robust and flexible. Recommended starting point when needing FIFO structure. | [Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms](https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf) | -| [Chase-Lev Work-Stealing Deque](src/ws_deque.mli) | Single-producer, multi-consumer dynamic-size double-ended queue (deque). Ideal for throughput-focused scheduling using per-core work distribution. Note, `pop` and `steal` follow different ordering (respectively LIFO and FIFO) and have different linearization contraints. | [Dynamic circular work-stealing deque](https://dl.acm.org/doi/10.1145/1073970.1073974) and [Correct and efficient work-stealing for weak memory models](https://dl.acm.org/doi/abs/10.1145/2442516.2442524)) | -| [SPSC Queue](src/spsc_queue.mli) | Simple single-producer single-consumer fixed-size queue. Thread-safe as long as at most one thread acts as producer and at most one as consumer at any single point in time. | | -| [MPMC Relaxed Queue](src/mpmc_relaxed_queue.mli) | Multi-producer, multi-consumer, fixed-size relaxed queue. Optimised for high number of threads. Not strictly FIFO. Note, it exposes two interfaces: a lockfree and a non-lockfree (albeit more practical) one. See the mli for details. | | -| [MPSC Queue](src/mpsc_queue.mli) | A multi-producer, single-consumer, thread-safe queue without support for cancellation. This makes a good data structure for a scheduler's run queue. It is used in [Eio](https://github.com/ocaml-multicore/eio). | It is a single consumer version of the queue described in [Implementing lock-free queues](https://people.cs.pitt.edu/~jacklange/teaching/cs2510-f12/papers/implementing_lock_free.pdf). | +- `Saturn` that includes every data structures and should be used by default if + you just want parallelism-safe data structures.. +- `Saturn_lockfree` that includes only lock-free data structures. + +The available data structures are : + +| Names | Names in `Saturn`
(in `Saturn_lockfree`) | What is it ? | Sources | +| ------------------------------------------------------------ | --------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| [Treiber stack](src_lockfree/treiber_stack.mli) | `Stack` (same) | A classic multi-producer multi-consumer stack, robust and flexible. Recommended starting point when needing a LIFO structure | | +| [Michael-Scott queue](src_lockfree/michael_scott_queue.mli) | `Queue` (same) | A classic multi-producer multi-consumer queue, robust and flexible. Recommended starting point when needing a FIFO structure. | [Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms](https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf) | +| [Chase-Lev Work-Stealing Dequeue](src_lockfree/ws_deque.mli) | `Work_stealing_deque` (same) | Single-producer, multi-consumer dynamic-size double-ended queue (deque). Ideal for throughput-focused scheduling using per-core work distribution. Note, `pop` and `steal` follow different ordering (respectively LIFO and FIFO) and have different linearization contraints. | [Dynamic circular work-stealing deque](https://dl.acm.org/doi/10.1145/1073970.1073974) and [Correct and efficient work-stealing for weak memory models](https://dl.acm.org/doi/abs/10.1145/2442516.2442524)) | +| [SPSC Queue](src_lockfree/spsc_queue.mli) | `Single_prod_single_`
`cons_queue` (same) | Simple single-producer single-consumer fixed-size queue. Thread-safe as long as at most one thread acts as producer and at most one as consumer at any single point in time. | | +| [MPMC bounded relaxed queue](src/mpmc_relaxed_queue.mli) | `Relaxed queue` (same) | Multi-producer, multi-consumer, fixed-size relaxed queue. Optimised for high number of threads. Not strictly FIFO. Note, it exposes two interfaces: a lockfree and a non-lockfree (albeit more practical) one. See the mli for details. | | +| [MPSC Queue](src_lockfree/mpsc_queue.mli) | `Single_consumer_queue` (same) | A multi-producer, single-consumer, thread-safe queue without support for cancellation. This makes a gooddata structure for a scheduler's run queue. It is used in [Eio](https://github.com/ocaml-multicore/eio). | It is a single consumer version of the queue described in [Implementing lock-free queues](https://people.cs.pitt.edu/~jacklange/teaching/cs2510-f12/papers/implementing_lock_free.pdf). | ## Usage `Saturn` can be installed from `opam`: `opam install saturn`. Sample usage of -`Ws_deque` is illustrated below. +`Work_stealing_deque` is illustrated below. ```ocaml -module Ws_deque = Ws_deque.M +module Ws_deque = Work_stealing_deque.M let q = Ws_deque.create () @@ -49,5 +56,5 @@ There is a number of benchmarks in `bench` directory. You can run them with ## Contributing -Contributions of more parallelism-safe data structures appreciated! Please create -issues/PRs to this repo. +Contributions are appreciated! If you intend to add a new data structure, please +read [this](CONTRIBUTING.md) before. diff --git a/dune-project b/dune-project index c50ca2f8..1b174e05 100644 --- a/dune-project +++ b/dune-project @@ -1,2 +1,8 @@ (lang dune 3.0) (name saturn) +(package + (name saturn) + (synopsis "Collection of parallelism-safe data structures for Multicore OCaml")) +(package + (name saturn_lockfree) + (synopsis "Collection of lock-free data structures for Multicore OCaml")) diff --git a/saturn.opam b/saturn.opam index 4947d89e..08bed7f1 100644 --- a/saturn.opam +++ b/saturn.opam @@ -16,7 +16,7 @@ depends: [ "qcheck-stm" {with-test & >= "0.2"} "qcheck-alcotest" {with-test & >= "0.18.1"} "alcotest" {with-test & >= "1.6.0"} - "yojson" {>= "2.0.2"} + "yojson" {with-test &>= "2.0.2"} "dscheck" {with-test & >= "0.1.0"} ] available: arch != "x86_32" & arch != "arm32" & arch != "ppc64" diff --git a/saturn_lockfree.opam b/saturn_lockfree.opam new file mode 100644 index 00000000..c1d073bb --- /dev/null +++ b/saturn_lockfree.opam @@ -0,0 +1,24 @@ +opam-version: "2.0" +maintainer:"KC Sivaramakrishnan " +authors: ["KC Sivaramakrishnan "] +homepage: "https://github.com/ocaml-multicore/saturn" +doc: "https://ocaml-multicore.github.io/saturn" +synopsis: "Lock-free data structures for multicore OCaml" +license: "ISC" +dev-repo: "git+https://github.com/ocaml-multicore/saturn.git" +bug-reports: "https://github.com/ocaml-multicore/saturn/issues" +tags: [] +depends: [ + "ocaml" {>= "4.12"} + "dune" {>= "3.0"} + "domain_shims" {>= "0.1.0"} + "qcheck" {with-test & >= "0.18.1"} + "qcheck-stm" {with-test & >= "0.2"} + "qcheck-alcotest" {with-test & >= "0.18.1"} + "alcotest" {with-test & >= "1.6.0"} + "yojson" {with-test &>= "2.0.2"} + "dscheck" {with-test & >= "0.1.0"} +] +available: arch != "x86_32" & arch != "arm32" & arch != "ppc64" +depopts: [] +build: ["dune" "build" "-p" name "-j" jobs] diff --git a/src/dune b/src/dune index efb4216d..ca2afd55 100644 --- a/src/dune +++ b/src/dune @@ -1,4 +1,4 @@ (library (name saturn) (public_name saturn) - (libraries domain_shims)) + (libraries saturn_lockfree domain_shims)) diff --git a/src/mpmc_relaxed_queue.ml b/src/mpmc_relaxed_queue.ml index 8c0ac96a..20b61bb1 100644 --- a/src/mpmc_relaxed_queue.ml +++ b/src/mpmc_relaxed_queue.ml @@ -1,140 +1,14 @@ -(* - # General idea - - It is the easiest to explain the general idea on an array of infinite size. - Let's start with that. Each element in such an array constitutes a single-use - exchange slot. Enqueuer increments [tail] and treats prior value as index of - its slot. Same for dequeuer and [head]. This effectively creates pairs - (enqueuer, dequeuer) assigned to the same slot. Enqueuer leaves the value in - the slot, dequer copies it out. - - Enqueuer never fails. It always gets a brand-new slot and places item in it. - Dequeuer, on the other hand, may witness an empty slot. That's because [head] - may jump behind [tail]. Remember, indices are implemented blindy. For now, - assume dequeuer simply spins on the empty slot until an item appears. +include Lockfree.Relaxed_queue - That's it. There's a few things flowing from this construction: - * Slots are atomic. This is where paired enqueuer and dequeuer communicate. - * [head] overshooting [tail] is a normal condition and that's good - we want - to keep operations on [head] and [tail] independent. - - # Finite array - - Now, to make it work in real-world, simply treat finite array as circular, - i.e. wrap around when reached the end. Slots are now re-used, so we need to be - more careful. - - Firstly, if there's too many items, enqueuer may witness a full slot. Let's assume - enqueuer simply spins on full slot until some dequeuer appears and takes the old - value. - - Secondly, in the case of overlap, there can be more than 2 threads (1x enqueuer, - 1x dequeuer) assigned to a single slot (imagine 10 enqueuers spinning on an 8-slot - array). In fact, it could be any number. Thus, all operations on slot have to use - CAS to ensure that no item is overwrriten on store and no item is dequeued by two - threads at once. - - Above works okay in practise, and there is some relevant literature, e.g. - (DOI: 10.1145/3437801.3441583) analyzed this particular design. There's also - plenty older papers looking at similar approaches - (e.g. DOI: 10.1145/2851141.2851168). - - Note, this design may violate FIFO (on overlap). The risk can be minimized by - ensuring size of array >> number of threads but it's never zero. - (github.com/rigtorp/MPMCQueue has a nice way of fixing this, we could add it). - - # Blocking (non-lockfree paths on full, empty) - - Up until now [push] and [pop] were allowed to block indefinitely on empty and full - queue. Overall, what can be done in those states? - - 1. Busy wait until able to finish. - 2. Rollback own index with CAS (unassign itself from slot). - 3. Move forward other index with CAS (assign itself to the same slot as opposite - action). - 4. Mark slot as burned - dequeue only. - - Which one then? - - Let's optimize for stability, i.e. some reasonable latency that won't get much worse - under heavy load. Busy wait is great because it does not cause any contention in the - hotspots ([head], [tail]). Thus, start with busy wait (1). If queue is busy and - moving fast, there is a fair chance that within, say, 30 spins, we'll manage to - complete action without having to add contention elsewhere. - - Once N busy-loops happen and nothing changes, we probably want to return even if its - costs. (2), (3) both allow that. (2) doesn't add contention to the other index like - (3) does. Say, there's a lot more dequeuers than enqueuers, if all dequeurs did (3), - they would add a fair amount of contention to the [tail] index and slow the - already-outnumbered enqueuers further. So, (2) > (3) for that reason. - - However, with just (2), some dequeuers will struggle to return. If many dequeuers - constatly try to pop an element and fail, they will form a chain. - - tl hd - | | - [.]-[A]-[B]-[C]-..-[X] - - For A to rollback, B has to rollback first. For B to rollback C has to rollback first. - - [A] is likely to experience a large latency spike. In such a case, it is easier for [A] - to do (3) rather than hope all other active dequeuers will unblock it at some point. - Thus, it's worthwile also trying to do (3) periodically. - - Thus, the current policy does (1) for a bit, then (1), (2) with periodic (3). - - What about burned slots (4)? - - It's present in the literature. Weakly I'm not a fan. If dequeuers are faster to remove - items than enqueuers supply them, slots burned by dequeuers are going to make enqueuers - do even more work. - - # Resizing - - The queue does not support resizing, but it can be simulated by wrapping it in a - lockfree list. -*) - -type 'a t = { - array : 'a Option.t Atomic.t Array.t; - head : int Atomic.t; - tail : int Atomic.t; - mask : int; -} - -let create ~size_exponent () : 'a t = - let size = 1 lsl size_exponent in - let array = Array.init size (fun _ -> Atomic.make None) in - let mask = size - 1 in - let head = Atomic.make 0 in - let tail = Atomic.make 0 in - { array; head; tail; mask } +module Spin = struct + let push = push + let pop = pop +end (* [ccas] A slightly nicer CAS. Tries without taking microarch lock first. Use on indices. *) let ccas cell seen v = if Atomic.get cell != seen then false else Atomic.compare_and_set cell seen v -module Spin = struct - let push { array; tail; mask; _ } item = - let tail_val = Atomic.fetch_and_add tail 1 in - let index = tail_val land mask in - let cell = Array.get array index in - while not (ccas cell None (Some item)) do - Domain.cpu_relax () - done - - let pop { array; head; mask; _ } = - let head_val = Atomic.fetch_and_add head 1 in - let index = head_val land mask in - let cell = Array.get array index in - let item = ref (Atomic.get cell) in - while Option.is_none !item || not (ccas cell !item None) do - Domain.cpu_relax (); - item := Atomic.get cell - done; - Option.get !item -end - module Not_lockfree = struct (* [spin_threshold] Number of times on spin on a slot before trying an exit strategy. *) let spin_threshold = 30 diff --git a/src/mpmc_relaxed_queue.mli b/src/mpmc_relaxed_queue.mli index 235fa36b..b7267926 100644 --- a/src/mpmc_relaxed_queue.mli +++ b/src/mpmc_relaxed_queue.mli @@ -1,5 +1,5 @@ (** - A multi-producer, multi-consumer, thread-safe, relaxed-FIFO queue. + A multi-producer, multi-consumer, thread-safe, bounded relaxed-FIFO queue. It exposes two interfaces: [Spin] and [Not_lockfree]. [Spin] is lock-free formally, but the property is achieved in a fairly counterintuitive way - diff --git a/src/saturn.ml b/src/saturn.ml index ca2e063a..a71a9903 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -26,10 +26,10 @@ Copyright (c) 2017, Nicolas ASSOUAD ######## *) -module Queue = Michael_scott_queue -module Stack = Treiber_stack -module Work_stealing_deque = Ws_deque -module Single_prod_single_cons_queue = Spsc_queue -module Single_consumer_queue = Mpsc_queue +module Queue = Lockfree.Queue +module Stack = Lockfree.Stack +module Work_stealing_deque = Lockfree.Work_stealing_deque +module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue +module Single_consumer_queue = Lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue -module Backoff = Backoff +module Backoff = Lockfree.Backoff diff --git a/src/saturn.mli b/src/saturn.mli index 923254f5..7a5aa1fa 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -30,13 +30,12 @@ Copyright (c) 2017, Nicolas ASSOUAD (** {1 Data structures} *) -module Queue = Michael_scott_queue -module Stack = Treiber_stack -module Work_stealing_deque = Ws_deque -module Single_prod_single_cons_queue = Spsc_queue -module Single_consumer_queue = Mpsc_queue +module Queue = Lockfree.Queue +module Stack = Lockfree.Stack +module Work_stealing_deque = Lockfree.Work_stealing_deque +module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue +module Single_consumer_queue = Lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue +module Backoff = Lockfree.Backoff (** {2 Other} *) - -module Backoff = Backoff diff --git a/src/ArrayExtra.ml b/src_lockfree/ArrayExtra.ml similarity index 100% rename from src/ArrayExtra.ml rename to src_lockfree/ArrayExtra.ml diff --git a/src/backoff.ml b/src_lockfree/backoff.ml similarity index 100% rename from src/backoff.ml rename to src_lockfree/backoff.ml diff --git a/src/backoff.mli b/src_lockfree/backoff.mli similarity index 100% rename from src/backoff.mli rename to src_lockfree/backoff.mli diff --git a/src_lockfree/dune b/src_lockfree/dune new file mode 100644 index 00000000..536acc06 --- /dev/null +++ b/src_lockfree/dune @@ -0,0 +1,4 @@ +(library + (name lockfree) + (public_name saturn_lockfree) + (libraries domain_shims)) diff --git a/src_lockfree/lockfree.ml b/src_lockfree/lockfree.ml new file mode 100644 index 00000000..ca2e063a --- /dev/null +++ b/src_lockfree/lockfree.ml @@ -0,0 +1,35 @@ +(*--------------------------------------------------------------------------- + Copyright (c) 2016 KC Sivaramakrishnan. All rights reserved. + Distributed under the ISC license, see terms at the end of the file. + %%NAME%% %%VERSION%% + ---------------------------------------------------------------------------*) + +(*--------------------------------------------------------------------------- + Copyright (c) 2016 KC Sivaramakrishnan + + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + ---------------------------------------------------------------------------*) + +(* +######## +Copyright (c) 2017, Nicolas ASSOUAD +######## +*) + +module Queue = Michael_scott_queue +module Stack = Treiber_stack +module Work_stealing_deque = Ws_deque +module Single_prod_single_cons_queue = Spsc_queue +module Single_consumer_queue = Mpsc_queue +module Relaxed_queue = Mpmc_relaxed_queue +module Backoff = Backoff diff --git a/src_lockfree/lockfree.mli b/src_lockfree/lockfree.mli new file mode 100644 index 00000000..d70939f5 --- /dev/null +++ b/src_lockfree/lockfree.mli @@ -0,0 +1,42 @@ +(*--------------------------------------------------------------------------- + Copyright (c) 2016 KC Sivaramakrishnan. All rights reserved. + Distributed under the ISC license, see terms at the end of the file. + %%NAME%% %%VERSION%% + ---------------------------------------------------------------------------*) + +(*--------------------------------------------------------------------------- + Copyright (c) 2016 KC Sivaramakrishnan + + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. + + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + ---------------------------------------------------------------------------*) + +(* +######## +Copyright (c) 2017, Nicolas ASSOUAD +######## +*) + +(** Lock-free data structures for Multicore OCaml *) + +(** {1 Data structures} *) + +module Queue = Michael_scott_queue +module Stack = Treiber_stack +module Work_stealing_deque = Ws_deque +module Single_prod_single_cons_queue = Spsc_queue +module Single_consumer_queue = Mpsc_queue +module Relaxed_queue = Mpmc_relaxed_queue + +(** {2 Other} *) + +module Backoff = Backoff diff --git a/src/michael_scott_queue.ml b/src_lockfree/michael_scott_queue.ml similarity index 100% rename from src/michael_scott_queue.ml rename to src_lockfree/michael_scott_queue.ml diff --git a/src/michael_scott_queue.mli b/src_lockfree/michael_scott_queue.mli similarity index 100% rename from src/michael_scott_queue.mli rename to src_lockfree/michael_scott_queue.mli diff --git a/src_lockfree/mpmc_relaxed_queue.ml b/src_lockfree/mpmc_relaxed_queue.ml new file mode 100644 index 00000000..db2ca43e --- /dev/null +++ b/src_lockfree/mpmc_relaxed_queue.ml @@ -0,0 +1,134 @@ +(* + # General idea + + It is the easiest to explain the general idea on an array of infinite size. + Let's start with that. Each element in such an array constitutes a single-use + exchange slot. Enqueuer increments [tail] and treats prior value as index of + its slot. Same for dequeuer and [head]. This effectively creates pairs + (enqueuer, dequeuer) assigned to the same slot. Enqueuer leaves the value in + the slot, dequer copies it out. + + Enqueuer never fails. It always gets a brand-new slot and places item in it. + Dequeuer, on the other hand, may witness an empty slot. That's because [head] + may jump behind [tail]. Remember, indices are implemented blindy. For now, + assume dequeuer simply spins on the empty slot until an item appears. + + That's it. There's a few things flowing from this construction: + * Slots are atomic. This is where paired enqueuer and dequeuer communicate. + * [head] overshooting [tail] is a normal condition and that's good - we want + to keep operations on [head] and [tail] independent. + + # Finite array + + Now, to make it work in real-world, simply treat finite array as circular, + i.e. wrap around when reached the end. Slots are now re-used, so we need to be + more careful. + + Firstly, if there's too many items, enqueuer may witness a full slot. Let's assume + enqueuer simply spins on full slot until some dequeuer appears and takes the old + value. + + Secondly, in the case of overlap, there can be more than 2 threads (1x enqueuer, + 1x dequeuer) assigned to a single slot (imagine 10 enqueuers spinning on an 8-slot + array). In fact, it could be any number. Thus, all operations on slot have to use + CAS to ensure that no item is overwrriten on store and no item is dequeued by two + threads at once. + + Above works okay in practise, and there is some relevant literature, e.g. + (DOI: 10.1145/3437801.3441583) analyzed this particular design. There's also + plenty older papers looking at similar approaches + (e.g. DOI: 10.1145/2851141.2851168). + + Note, this design may violate FIFO (on overlap). The risk can be minimized by + ensuring size of array >> number of threads but it's never zero. + (github.com/rigtorp/MPMCQueue has a nice way of fixing this, we could add it). + + # Blocking (non-lockfree paths on full, empty) + + Up until now [push] and [pop] were allowed to block indefinitely on empty and full + queue. Overall, what can be done in those states? + + 1. Busy wait until able to finish. + 2. Rollback own index with CAS (unassign itself from slot). + 3. Move forward other index with CAS (assign itself to the same slot as opposite + action). + 4. Mark slot as burned - dequeue only. + + Which one then? + + Let's optimize for stability, i.e. some reasonable latency that won't get much worse + under heavy load. Busy wait is great because it does not cause any contention in the + hotspots ([head], [tail]). Thus, start with busy wait (1). If queue is busy and + moving fast, there is a fair chance that within, say, 30 spins, we'll manage to + complete action without having to add contention elsewhere. + + Once N busy-loops happen and nothing changes, we probably want to return even if its + costs. (2), (3) both allow that. (2) doesn't add contention to the other index like + (3) does. Say, there's a lot more dequeuers than enqueuers, if all dequeurs did (3), + they would add a fair amount of contention to the [tail] index and slow the + already-outnumbered enqueuers further. So, (2) > (3) for that reason. + + However, with just (2), some dequeuers will struggle to return. If many dequeuers + constatly try to pop an element and fail, they will form a chain. + + tl hd + | | + [.]-[A]-[B]-[C]-..-[X] + + For A to rollback, B has to rollback first. For B to rollback C has to rollback first. + + [A] is likely to experience a large latency spike. In such a case, it is easier for [A] + to do (3) rather than hope all other active dequeuers will unblock it at some point. + Thus, it's worthwile also trying to do (3) periodically. + + Thus, the current policy does (1) for a bit, then (1), (2) with periodic (3). + + What about burned slots (4)? + + It's present in the literature. Weakly I'm not a fan. If dequeuers are faster to remove + items than enqueuers supply them, slots burned by dequeuers are going to make enqueuers + do even more work. + + # Resizing + + The queue does not support resizing, but it can be simulated by wrapping it in a + lockfree list. +*) + +type 'a t = { + array : 'a Option.t Atomic.t Array.t; + head : int Atomic.t; + tail : int Atomic.t; + mask : int; +} + +let create ~size_exponent () : 'a t = + let size = 1 lsl size_exponent in + let array = Array.init size (fun _ -> Atomic.make None) in + let mask = size - 1 in + let head = Atomic.make 0 in + let tail = Atomic.make 0 in + { array; head; tail; mask } + +(* [ccas] A slightly nicer CAS. Tries without taking microarch lock first. Use on indices. *) +let ccas cell seen v = + if Atomic.get cell != seen then false else Atomic.compare_and_set cell seen v + +let push { array; tail; mask; _ } item = + let tail_val = Atomic.fetch_and_add tail 1 in + let index = tail_val land mask in + let cell = Array.get array index in + while not (ccas cell None (Some item)) do + Domain.cpu_relax () + done + +let pop { array; head; mask; _ } = + let head_val = Atomic.fetch_and_add head 1 in + let index = head_val land mask in + let cell = Array.get array index in + let item = ref (Atomic.get cell) in + while Option.is_none !item || not (ccas cell !item None) do + Domain.cpu_relax (); + item := Atomic.get cell + done; + Option.get !item diff --git a/src_lockfree/mpmc_relaxed_queue.mli b/src_lockfree/mpmc_relaxed_queue.mli new file mode 100644 index 00000000..04049734 --- /dev/null +++ b/src_lockfree/mpmc_relaxed_queue.mli @@ -0,0 +1,36 @@ +(** + A multi-producer, multi-consumer, thread-safe, bounded relaxed-FIFO queue. + + This interface is a subset of the one in `Saturn.Relaxed_queue` + that exposes a formally lock-free interface as per the [A + lock-free relaxed concurrent queue for fast work distribution] + paper. + + [push] and [pop] are said to be `lock-free formally`, because the + property is achieved in a fairly counterintuitive way - by using + the fact that lock-freedom does not impose any constraints on + partial methods. In simple words, an invocation of function that + cannot logically terminate (`push` on full queue, `pop` on empty + queue), it is allowed to *busy-wait* until the precondition is + meet. +*) + +type 'a t = private { + array : 'a Option.t Atomic.t Array.t; + head : int Atomic.t; + tail : int Atomic.t; + mask : int; +} +(** A queue of items of type ['a]. Implementation exposed for testing. *) + +val create : size_exponent:int -> unit -> 'a t +(** [create ~size_exponent:int] creates an empty queue of size + [2^size_exponent]. *) + +val push : 'a t -> 'a -> unit +(** [push t x] adds [x] to the tail of the queue. If the queue is full, [push] + busy-waits until another thread removes an item. *) + +val pop : 'a t -> 'a +(** [pop t] removes an item from the head of the queue. If the queue is empty, + [pop] busy-waits until an item appear. *) diff --git a/src/mpsc_queue.ml b/src_lockfree/mpsc_queue.ml similarity index 100% rename from src/mpsc_queue.ml rename to src_lockfree/mpsc_queue.ml diff --git a/src/mpsc_queue.mli b/src_lockfree/mpsc_queue.mli similarity index 100% rename from src/mpsc_queue.mli rename to src_lockfree/mpsc_queue.mli diff --git a/src/spsc_queue.ml b/src_lockfree/spsc_queue.ml similarity index 100% rename from src/spsc_queue.ml rename to src_lockfree/spsc_queue.ml diff --git a/src/spsc_queue.mli b/src_lockfree/spsc_queue.mli similarity index 100% rename from src/spsc_queue.mli rename to src_lockfree/spsc_queue.mli diff --git a/src/treiber_stack.ml b/src_lockfree/treiber_stack.ml similarity index 100% rename from src/treiber_stack.ml rename to src_lockfree/treiber_stack.ml diff --git a/src/treiber_stack.mli b/src_lockfree/treiber_stack.mli similarity index 100% rename from src/treiber_stack.mli rename to src_lockfree/treiber_stack.mli diff --git a/src/ws_deque.ml b/src_lockfree/ws_deque.ml similarity index 100% rename from src/ws_deque.ml rename to src_lockfree/ws_deque.ml diff --git a/src/ws_deque.mli b/src_lockfree/ws_deque.mli similarity index 100% rename from src/ws_deque.mli rename to src_lockfree/ws_deque.mli diff --git a/test/michael_scott_queue/dune b/test/michael_scott_queue/dune index 11fca835..16459e6f 100644 --- a/test/michael_scott_queue/dune +++ b/test/michael_scott_queue/dune @@ -1,8 +1,8 @@ (rule - (copy ../../src/backoff.ml backoff.ml)) + (copy ../../src_lockfree/backoff.ml backoff.ml)) (rule - (copy ../../src/michael_scott_queue.ml michael_scott_queue.ml)) + (copy ../../src_lockfree/michael_scott_queue.ml michael_scott_queue.ml)) (test (name michael_scott_queue_dscheck) diff --git a/test/mpsc_queue/dune b/test/mpsc_queue/dune index df8412aa..0a13202d 100644 --- a/test/mpsc_queue/dune +++ b/test/mpsc_queue/dune @@ -1,5 +1,5 @@ (rule - (copy ../../src/mpsc_queue.ml mpsc_queue.ml)) + (copy ../../src_lockfree/mpsc_queue.ml mpsc_queue.ml)) (test (name mpsc_queue_dscheck) diff --git a/seqtest/.gitignore b/test/seqtest/.gitignore similarity index 100% rename from seqtest/.gitignore rename to test/seqtest/.gitignore diff --git a/seqtest/Makefile b/test/seqtest/Makefile similarity index 100% rename from seqtest/Makefile rename to test/seqtest/Makefile diff --git a/seqtest/Makefile.monolith b/test/seqtest/Makefile.monolith similarity index 100% rename from seqtest/Makefile.monolith rename to test/seqtest/Makefile.monolith diff --git a/seqtest/README.md b/test/seqtest/README.md similarity index 100% rename from seqtest/README.md rename to test/seqtest/README.md diff --git a/seqtest/dune b/test/seqtest/dune similarity index 100% rename from seqtest/dune rename to test/seqtest/dune diff --git a/seqtest/seqtest.ml b/test/seqtest/seqtest.ml similarity index 100% rename from seqtest/seqtest.ml rename to test/seqtest/seqtest.ml diff --git a/test/spsc_queue/dune b/test/spsc_queue/dune index 0b14b4c3..e406a8dd 100644 --- a/test/spsc_queue/dune +++ b/test/spsc_queue/dune @@ -1,5 +1,5 @@ (rule - (copy ../../src/spsc_queue.ml spsc_queue.ml)) + (copy ../../src_lockfree/spsc_queue.ml spsc_queue.ml)) (test (name spsc_queue_dscheck) diff --git a/test/treiber_stack/dune b/test/treiber_stack/dune index 22cbcf84..274c7ceb 100644 --- a/test/treiber_stack/dune +++ b/test/treiber_stack/dune @@ -1,8 +1,8 @@ (rule - (copy ../../src/backoff.ml backoff.ml)) + (copy ../../src_lockfree/backoff.ml backoff.ml)) (rule - (copy ../../src/treiber_stack.ml treiber_stack.ml)) + (copy ../../src_lockfree/treiber_stack.ml treiber_stack.ml)) (test (name treiber_stack_dscheck) diff --git a/test/ws_deque/dune b/test/ws_deque/dune index 06515680..a4a159c2 100644 --- a/test/ws_deque/dune +++ b/test/ws_deque/dune @@ -1,8 +1,8 @@ (rule - (copy ../../src/ArrayExtra.ml ArrayExtra.ml)) + (copy ../../src_lockfree/ArrayExtra.ml ArrayExtra.ml)) (rule - (copy ../../src/ws_deque.ml ws_deque.ml)) + (copy ../../src_lockfree/ws_deque.ml ws_deque.ml)) (test (name ws_deque_dscheck) From b485b742ac7b38c7541621dffc3b654415c04d01 Mon Sep 17 00:00:00 2001 From: Sudha Parimala Date: Mon, 10 Jul 2023 19:05:57 +0530 Subject: [PATCH 16/22] Prepare release --- CHANGES.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index f3349e4a..f012472a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,10 +1,11 @@ -# Release notes - -All notable changes to this project will be documented in this file. - -## Not released +## 0.4.0 - Add docs and rename/refactor to add a lockfree package (@lyrm) +- CI clean up and set up Windows CI (@lyrm) +- Adopt OCaml Code of Conduct (@Sudha247) +- Mark alcotest as a test dependency (@Khady) +- Set QCHECK_MSG_INTERVAL to avoid clutter in CI logs (@jmid) +- Fix space leaks in MS Queue (@polytypic, @lyrm) - Add STM tests for current data structures (@lyrm, @jmid) ## 0.3.1 From 2aa31c21faec9cc4d2466d345b970f4fd7ed80e3 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 26 Jul 2023 14:35:47 +0200 Subject: [PATCH 17/22] Remove .merlin and .ocp-indent files. --- .merlin | 4 ---- .ocp-indent | 1 - 2 files changed, 5 deletions(-) delete mode 100644 .merlin delete mode 100644 .ocp-indent diff --git a/.merlin b/.merlin deleted file mode 100644 index 0e0495c3..00000000 --- a/.merlin +++ /dev/null @@ -1,4 +0,0 @@ -PKG bytes -S src -S test -B _build/** diff --git a/.ocp-indent b/.ocp-indent deleted file mode 100644 index 6c5b8f4d..00000000 --- a/.ocp-indent +++ /dev/null @@ -1 +0,0 @@ -strict_with=always,match_clause=4,strict_else=never From 0401757c4f06b95ea9db6111873c0f365e9e32c8 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 26 Jul 2023 14:11:14 +0200 Subject: [PATCH 18/22] Correct issue caused by saturn_lockfree module beeing named Lockfree. --- src/dune | 2 +- src/mpmc_relaxed_queue.ml | 2 +- src/saturn.ml | 15 +++++++++------ src/saturn.mli | 15 +++++++++------ src_lockfree/dune | 2 +- src_lockfree/{lockfree.ml => saturn_lockfree.ml} | 0 .../{lockfree.mli => saturn_lockfree.mli} | 0 7 files changed, 21 insertions(+), 15 deletions(-) rename src_lockfree/{lockfree.ml => saturn_lockfree.ml} (100%) rename src_lockfree/{lockfree.mli => saturn_lockfree.mli} (100%) diff --git a/src/dune b/src/dune index ca2afd55..322a19be 100644 --- a/src/dune +++ b/src/dune @@ -1,4 +1,4 @@ (library (name saturn) (public_name saturn) - (libraries saturn_lockfree domain_shims)) + (libraries saturn_lockfree)) diff --git a/src/mpmc_relaxed_queue.ml b/src/mpmc_relaxed_queue.ml index 20b61bb1..afb139c5 100644 --- a/src/mpmc_relaxed_queue.ml +++ b/src/mpmc_relaxed_queue.ml @@ -1,4 +1,4 @@ -include Lockfree.Relaxed_queue +include Saturn_lockfree.Relaxed_queue module Spin = struct let push = push diff --git a/src/saturn.ml b/src/saturn.ml index a71a9903..d3b71e46 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -26,10 +26,13 @@ Copyright (c) 2017, Nicolas ASSOUAD ######## *) -module Queue = Lockfree.Queue -module Stack = Lockfree.Stack -module Work_stealing_deque = Lockfree.Work_stealing_deque -module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue -module Single_consumer_queue = Lockfree.Single_consumer_queue +module Queue = Saturn_lockfree.Queue +module Stack = Saturn_lockfree.Stack +module Work_stealing_deque = Saturn_lockfree.Work_stealing_deque + +module Single_prod_single_cons_queue = + Saturn_lockfree.Single_prod_single_cons_queue + +module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue -module Backoff = Lockfree.Backoff +module Backoff = Saturn_lockfree.Backoff diff --git a/src/saturn.mli b/src/saturn.mli index 7a5aa1fa..1a9d56f5 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -30,12 +30,15 @@ Copyright (c) 2017, Nicolas ASSOUAD (** {1 Data structures} *) -module Queue = Lockfree.Queue -module Stack = Lockfree.Stack -module Work_stealing_deque = Lockfree.Work_stealing_deque -module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue -module Single_consumer_queue = Lockfree.Single_consumer_queue +module Queue = Saturn_lockfree.Queue +module Stack = Saturn_lockfree.Stack +module Work_stealing_deque = Saturn_lockfree.Work_stealing_deque + +module Single_prod_single_cons_queue = + Saturn_lockfree.Single_prod_single_cons_queue + +module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue module Relaxed_queue = Mpmc_relaxed_queue -module Backoff = Lockfree.Backoff +module Backoff = Saturn_lockfree.Backoff (** {2 Other} *) diff --git a/src_lockfree/dune b/src_lockfree/dune index 536acc06..7a76425e 100644 --- a/src_lockfree/dune +++ b/src_lockfree/dune @@ -1,4 +1,4 @@ (library - (name lockfree) + (name saturn_lockfree) (public_name saturn_lockfree) (libraries domain_shims)) diff --git a/src_lockfree/lockfree.ml b/src_lockfree/saturn_lockfree.ml similarity index 100% rename from src_lockfree/lockfree.ml rename to src_lockfree/saturn_lockfree.ml diff --git a/src_lockfree/lockfree.mli b/src_lockfree/saturn_lockfree.mli similarity index 100% rename from src_lockfree/lockfree.mli rename to src_lockfree/saturn_lockfree.mli From 4fe464dc1603e18042953fa8a723c946c23a1bc8 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 5 Jul 2023 17:49:43 +0200 Subject: [PATCH 19/22] Add a barrier module in tests to replace the use of semaphores. --- test/README.md | 3 +- test/barrier/barrier.ml | 19 +++++++ test/barrier/barrier.mli | 52 +++++++++++++++++++ test/barrier/dune | 2 + test/michael_scott_queue/dune | 2 +- .../qcheck_michael_scott_queue.ml | 16 +++--- test/mpsc_queue/dune | 2 +- test/mpsc_queue/qcheck_mpsc_queue.ml | 51 +++++------------- test/spsc_queue/dune | 2 +- test/spsc_queue/qcheck_spsc_queue.ml | 11 ++-- test/treiber_stack/dune | 2 +- test/treiber_stack/qcheck_treiber_stack.ml | 24 ++++----- test/ws_deque/dune | 2 +- test/ws_deque/qcheck_ws_deque.ml | 35 +++++-------- 14 files changed, 127 insertions(+), 96 deletions(-) create mode 100644 test/barrier/barrier.ml create mode 100644 test/barrier/barrier.mli create mode 100644 test/barrier/dune diff --git a/test/README.md b/test/README.md index ae253e22..3c8640fd 100644 --- a/test/README.md +++ b/test/README.md @@ -25,7 +25,8 @@ runs with parallelism: - make a domain repeat its operations. In particular, that usually works well when testing a single function. -- use a semaphore to make all domains wait for each other before starting (see +- use the provided [barrier](barrier/barrier.mli) module to make all domains + wait for each other before starting (see [these tests for example) ](ws_deque/qcheck_ws_deque.ml)). - if you are still not sure your tests have a good chance to run in parallel, try it in the top level, and use print or outputs to understand what is diff --git a/test/barrier/barrier.ml b/test/barrier/barrier.ml new file mode 100644 index 00000000..259d688b --- /dev/null +++ b/test/barrier/barrier.ml @@ -0,0 +1,19 @@ +type t = { waiters : int Atomic.t; size : int; passed : int Atomic.t } + +let create n = { waiters = Atomic.make 0; size = n; passed = Atomic.make 0 } + +let await { waiters; size; passed } = + (* Wait for the barrier to release the previous group *) + while Atomic.get waiters = size do + Domain.cpu_relax () + done; + (* Add itself in the waiters group *) + Atomic.incr waiters; + (* Wait for enough waiters to arrive *) + while Atomic.get waiters < size do + Domain.cpu_relax () + done; + (* Have passed. Increased [passed]. If last one to pass, reset the barrier. *) + if Atomic.fetch_and_add passed 1 = size - 1 then ( + Atomic.set passed 0; + Atomic.set waiters 0) diff --git a/test/barrier/barrier.mli b/test/barrier/barrier.mli new file mode 100644 index 00000000..14b4d833 --- /dev/null +++ b/test/barrier/barrier.mli @@ -0,0 +1,52 @@ +(** A barrier is a synchronisation tool. + + A barrier of capacity [n] blocks domains until [n] of them are + waiting. Then these [n] domains can pass. Then the barrier is + reset. + + Note that this barrier is not starvation-free if there is more + domains trying to pass it than its capacity. + + This module has been written to help make sure that in `qcheck` tests and + unitary tests, multiple domains are actually running in parallel. + + + If you try this : + {[ + let example nb_domain = + let printer i () = + Format.printf "Domain spawn in %dth position@." i + in + let domains = List.init nb_domain (fun i -> Domain.spawn (printer i)) in + List.iter Domain.join domains + ]} + + you are most likely going to get the number in order (or almost), + because printing a line is way much cheaper than spawning a + domain. + + Whereas with the barrier, you should get a random order : + {[ + let example_with_barrier nb_domain = + let barrier = Barrier.create nb_domain in + + let printer i () = + Barrier.await barrier; + Format.printf "Domain spawn in %dth position@." i + in + + let domains = List.init nb_domain (fun i -> Domain.spawn (printer i)) in + + List.iter Domain.join domains + ]} +*) + +type t + +val create : int -> t +(** [create c] returns a barrier of capacity [c]. *) + +val await : t -> unit +(** A domain calling [await barrier] will only be able to + progress past this function once the number of domains waiting at + the barrier is egal to its capacity . *) diff --git a/test/barrier/dune b/test/barrier/dune new file mode 100644 index 00000000..ef5b99e4 --- /dev/null +++ b/test/barrier/dune @@ -0,0 +1,2 @@ +(library + (name barrier)) diff --git a/test/michael_scott_queue/dune b/test/michael_scott_queue/dune index 16459e6f..73b2d74c 100644 --- a/test/michael_scott_queue/dune +++ b/test/michael_scott_queue/dune @@ -11,7 +11,7 @@ (test (name qcheck_michael_scott_queue) - (libraries saturn qcheck qcheck-alcotest) + (libraries saturn barrier qcheck qcheck-alcotest) (modules qcheck_michael_scott_queue)) (test diff --git a/test/michael_scott_queue/qcheck_michael_scott_queue.ml b/test/michael_scott_queue/qcheck_michael_scott_queue.ml index 70a4cd55..4b1add80 100644 --- a/test/michael_scott_queue/qcheck_michael_scott_queue.ml +++ b/test/michael_scott_queue/qcheck_michael_scott_queue.ml @@ -85,7 +85,7 @@ let tests_two_domains = (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) let queue = create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* Using these lists instead of a random one enables to check for more properties. *) @@ -103,13 +103,11 @@ let tests_two_domains = let domain1 = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; work lpush1) in let popped2 = - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; work lpush2 in @@ -145,7 +143,7 @@ let tests_two_domains = (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) let queue = create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in let lpush1 = List.init npush1 (fun i -> i) in let lpush2 = List.init npush2 (fun i -> i + npush1) in @@ -173,13 +171,11 @@ let tests_two_domains = let domain1 = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; work lpush1) in let popped2 = - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; work lpush2 in diff --git a/test/mpsc_queue/dune b/test/mpsc_queue/dune index 0a13202d..646e0781 100644 --- a/test/mpsc_queue/dune +++ b/test/mpsc_queue/dune @@ -8,7 +8,7 @@ (test (name qcheck_mpsc_queue) - (libraries saturn qcheck qcheck-alcotest) + (libraries saturn barrier qcheck qcheck-alcotest) (modules qcheck_mpsc_queue)) (test diff --git a/test/mpsc_queue/qcheck_mpsc_queue.ml b/test/mpsc_queue/qcheck_mpsc_queue.ml index 0484e174..be2af596 100644 --- a/test/mpsc_queue/qcheck_mpsc_queue.ml +++ b/test/mpsc_queue/qcheck_mpsc_queue.ml @@ -295,12 +295,12 @@ let tests_one_consumer_one_producer = (fun (lpush, npop) -> (* Initialization *) let queue = Mpsc_queue.create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* Producer pushes. *) let producer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; try List.iter (fun elt -> @@ -312,15 +312,11 @@ let tests_one_consumer_one_producer = in (* Waiting to make sure the producer can start *) - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; (* Consumer pops. *) let popped = extract_n queue npop (npop + 1) in - let closed = Domain.join producer in - let popped_value = List.filter (function `Some _ -> true | _ -> false) popped in @@ -341,12 +337,12 @@ let tests_one_consumer_one_producer = (fun (lpush, lpush_head) -> (* Initialization *) let queue = Mpsc_queue.create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* Producer pushes. *) let producer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; try List.iter (fun elt -> @@ -358,9 +354,7 @@ let tests_one_consumer_one_producer = in (* Waiting to make sure the producer can start *) - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; List.iter (fun elt -> Mpsc_queue.push_head queue elt) lpush_head; @@ -376,18 +370,17 @@ let tests_one_consumer_one_producer = = list_some (lpush_head |> List.rev) && keep_n_last (List.length lpush) all_pushed = list_some lpush); (* TEST 4 - one consumer one producer - Consumer push then close while consumer pop until the queue is empty and closed. *) Test.make ~name:"par_pop_push2" (list int) (fun lpush -> (* Initialisation*) let queue = Mpsc_queue.create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* Sequential [push_head] *) let producer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; let res = try List.iter @@ -402,14 +395,9 @@ let tests_one_consumer_one_producer = res) in - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; - + Barrier.await barrier; let popped = popped_until_empty_and_closed queue in - let unexpected_closed = Domain.join producer in - let popped_value = List.filter (function Some _ -> true | _ -> false) popped in @@ -430,14 +418,10 @@ let tests_one_consumer_two_producers = (* Initialization *) let npush1, npush2 = (List.length lpush1, List.length lpush2) in let queue = Mpsc_queue.create () in - let sema = Semaphore.Counting.make 2 in + let barrier = Barrier.create 2 in let multi_push lpush = - Semaphore.Counting.acquire sema; - while Semaphore.Counting.try_acquire sema do - Semaphore.Counting.release sema; - Domain.cpu_relax () - done; + Barrier.await barrier; try List.iter (fun elt -> @@ -502,14 +486,10 @@ let tests_one_consumer_two_producers = (* Initialization *) let npush1, npush2 = (List.length lpush1, List.length lpush2) in let queue = Mpsc_queue.create () in - let sema = Semaphore.Counting.make 2 in + let barrier = Barrier.create 3 in let guard_push lpush = - Semaphore.Counting.acquire sema; - while Semaphore.Counting.try_acquire sema do - Semaphore.Counting.release sema; - Domain.cpu_relax () - done; + Barrier.await barrier; let closed_when_pushing = try List.iter @@ -534,10 +514,7 @@ let tests_one_consumer_two_producers = (* Waiting to make sure the producers have time to start. However, as the consumer will [pop] until one of the producer closes the queue, it is not a requirement to wait here. *) - while Semaphore.Counting.try_acquire sema do - Semaphore.Counting.release sema; - Domain.cpu_relax () - done; + Barrier.await barrier; let popped = popped_until_empty_and_closed queue in diff --git a/test/spsc_queue/dune b/test/spsc_queue/dune index e406a8dd..95b91d27 100644 --- a/test/spsc_queue/dune +++ b/test/spsc_queue/dune @@ -13,7 +13,7 @@ (test (name qcheck_spsc_queue) - (libraries saturn qcheck "qcheck-alcotest") + (libraries saturn barrier qcheck "qcheck-alcotest") (modules qcheck_spsc_queue)) (test diff --git a/test/spsc_queue/qcheck_spsc_queue.ml b/test/spsc_queue/qcheck_spsc_queue.ml index e3050468..069ca398 100644 --- a/test/spsc_queue/qcheck_spsc_queue.ml +++ b/test/spsc_queue/qcheck_spsc_queue.ml @@ -62,23 +62,20 @@ let tests = assume (List.length l + List.length l' < size_max); (* Initialization *) + let barrier = Barrier.create 2 in let q = Spsc_queue.create ~size_exponent in List.iter (Spsc_queue.push q) l; (* Consumer pops *) - let sema = Semaphore.Binary.make false in let consumer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; pop_n_times q npop) in let producer = Domain.spawn (fun () -> - (* Making sure the consumer can start *) - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; (* Main domain pushes.*) List.iter (fun elt -> @@ -95,7 +92,7 @@ let tests = List.length popped = npop && popped_val = keep_n_first (List.length popped_val) (l @ l'))); (* TEST 3 - one producer, one consumer: - Checks that pushing to much raise exception Full. *) + Checks that pushing too much raise exception Full. *) QCheck.( Test.make ~name:"push_full" (list int) (fun l -> let size_exponent = 4 in diff --git a/test/treiber_stack/dune b/test/treiber_stack/dune index 274c7ceb..2b6669a9 100644 --- a/test/treiber_stack/dune +++ b/test/treiber_stack/dune @@ -11,7 +11,7 @@ (test (name qcheck_treiber_stack) - (libraries saturn qcheck qcheck-alcotest) + (libraries saturn barrier qcheck qcheck-alcotest) (modules qcheck_treiber_stack)) (test diff --git a/test/treiber_stack/qcheck_treiber_stack.ml b/test/treiber_stack/qcheck_treiber_stack.ml index eced6fdc..4497d1fe 100644 --- a/test/treiber_stack/qcheck_treiber_stack.ml +++ b/test/treiber_stack/qcheck_treiber_stack.ml @@ -58,18 +58,16 @@ let tests_one_consumer_one_producer = Test.make ~count:10_000 ~name:"parallel" (list int) (fun lpush -> (* Initialization *) let stack = create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* Producer pushes. *) let producer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; List.iter (push stack) lpush) in - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; for _ = 1 to List.length lpush do while Option.is_none (pop stack) do () @@ -91,7 +89,7 @@ let tests_two_domains = (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) let stack = create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in let lpush1 = List.init npush1 (fun i -> i) in let lpush2 = List.init npush2 (fun i -> i + npush1) in @@ -107,13 +105,11 @@ let tests_two_domains = let domain1 = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; work lpush1) in let popped2 = - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; work lpush2 in @@ -143,7 +139,7 @@ let tests_two_domains = let lpush1 = List.init npush1 (fun i -> i) in let lpush2 = List.init npush2 (fun i -> i + npush1) in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in let work lpush = let consecutive_pop = ref 0 in @@ -168,13 +164,11 @@ let tests_two_domains = let domain1 = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; work lpush1) in let popped2 = - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + Barrier.await barrier; work lpush2 in diff --git a/test/ws_deque/dune b/test/ws_deque/dune index a4a159c2..5bdd4e3a 100644 --- a/test/ws_deque/dune +++ b/test/ws_deque/dune @@ -16,7 +16,7 @@ (test (name qcheck_ws_deque) - (libraries saturn qcheck "qcheck-alcotest") + (libraries barrier saturn qcheck "qcheck-alcotest") (modules qcheck_ws_deque)) (test diff --git a/test/ws_deque/qcheck_ws_deque.ml b/test/ws_deque/qcheck_ws_deque.ml index 2cf27e03..38992901 100644 --- a/test/ws_deque/qcheck_ws_deque.ml +++ b/test/ws_deque/qcheck_ws_deque.ml @@ -111,14 +111,14 @@ let tests_one_producer_one_stealer = (fun (l, n) -> (* Initialization *) let deque = Ws_deque.create () in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in (* The stealer domain steals n times. If a value [v] is stolen, it is registered as [Some v] in the returned list whereas any [Exit] raised is registered as a [None].*) let stealer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; let steal' deque = let res = try Some (Ws_deque.steal deque) with Exit -> None @@ -128,12 +128,9 @@ let tests_one_producer_one_stealer = in extract_n_of_deque deque steal' n) in - (* The semaphore is used to make sure the stealer domain has a - chance to begin its works before the main domain has finished - its. *) - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + + Barrier.await barrier; + (* Main domain pushes.*) List.iter (fun elt -> @@ -171,7 +168,7 @@ let tests_one_producer_one_stealer = assume (nsteal + npop > List.length l); (* Initialization - sequential pushes*) let deque = deque_of_list l in - let sema = Semaphore.Binary.make false in + let barrier = Barrier.create 2 in let _ = Random.self_init () in let pop' deque = let res = try Some (Ws_deque.pop deque) with Exit -> None in @@ -184,7 +181,7 @@ let tests_one_producer_one_stealer = raised, it is registered as a [None].*) let stealer = Domain.spawn (fun () -> - Semaphore.Binary.release sema; + Barrier.await barrier; let steal' deque = let res = try Some (Ws_deque.steal deque) with Exit -> None @@ -194,11 +191,9 @@ let tests_one_producer_one_stealer = in extract_n_of_deque deque steal' nsteal) in - (* The semaphore is used to make sure the stealer domain has a - chance to begin its works before the main domain has finished its. *) - while not (Semaphore.Binary.try_acquire sema) do - Domain.cpu_relax () - done; + + Barrier.await barrier; + (* Main domain pops and builds a list of popped values. *) let pop_list = extract_n_of_deque deque pop' npop in @@ -231,16 +226,14 @@ let tests_one_producer_two_stealers = (fun (l, (ns1, ns2)) -> (* Initialization *) let deque = deque_of_list l in - let sema = Semaphore.Counting.make 2 in + let barrier = Barrier.create 2 in (* Steal calls *) let multiple_steal deque nsteal = - Semaphore.Counting.acquire sema; + Barrier.await barrier; + let res = Array.make nsteal None in - while Semaphore.Counting.try_acquire sema do - Semaphore.Counting.release sema; - Domain.cpu_relax () - done; + for i = 0 to nsteal - 1 do res.(i) <- (try Some (Ws_deque.steal deque) with Exit -> None); Domain.cpu_relax () From 46e1662c77f6945c125b66989dae72d4a1f6a788 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 31 Jul 2023 11:12:18 +0200 Subject: [PATCH 20/22] Format. --- test/barrier/barrier.ml | 3 ++- test/barrier/barrier.mli | 20 +++++++++----------- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/test/barrier/barrier.ml b/test/barrier/barrier.ml index 259d688b..32b2e497 100644 --- a/test/barrier/barrier.ml +++ b/test/barrier/barrier.ml @@ -13,7 +13,8 @@ let await { waiters; size; passed } = while Atomic.get waiters < size do Domain.cpu_relax () done; - (* Have passed. Increased [passed]. If last one to pass, reset the barrier. *) + (* Have passed. Increased [passed]. If last one to pass, reset the + barrier. *) if Atomic.fetch_and_add passed 1 = size - 1 then ( Atomic.set passed 0; Atomic.set waiters 0) diff --git a/test/barrier/barrier.mli b/test/barrier/barrier.mli index 14b4d833..58007047 100644 --- a/test/barrier/barrier.mli +++ b/test/barrier/barrier.mli @@ -1,11 +1,10 @@ (** A barrier is a synchronisation tool. - A barrier of capacity [n] blocks domains until [n] of them are - waiting. Then these [n] domains can pass. Then the barrier is - reset. + A barrier of capacity [n] blocks domains until [n] of them are waiting. Then + these [n] domains can pass. Then the barrier is reset. - Note that this barrier is not starvation-free if there is more - domains trying to pass it than its capacity. + Note that this barrier is not starvation-free if there is more domains + trying to pass it than its capacity. This module has been written to help make sure that in `qcheck` tests and unitary tests, multiple domains are actually running in parallel. @@ -21,9 +20,8 @@ List.iter Domain.join domains ]} - you are most likely going to get the number in order (or almost), - because printing a line is way much cheaper than spawning a - domain. + you are most likely going to get the number in order (or almost), because + printing a line is way much cheaper than spawning a domain. Whereas with the barrier, you should get a random order : {[ @@ -47,6 +45,6 @@ val create : int -> t (** [create c] returns a barrier of capacity [c]. *) val await : t -> unit -(** A domain calling [await barrier] will only be able to - progress past this function once the number of domains waiting at - the barrier is egal to its capacity . *) +(** A domain calling [await barrier] will only be able to progress past this + function once the number of domains waiting at the barrier is egal to its + capacity . *) From a519b4b631f6bf9aa7bb513ca85f4de06ebdd949 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 31 Jul 2023 16:12:20 +0200 Subject: [PATCH 21/22] Improve documentation and changes barrier implementation a bit for optimization. --- test/barrier/barrier.ml | 17 +++++++---------- test/barrier/barrier.mli | 13 +++++++++++++ 2 files changed, 20 insertions(+), 10 deletions(-) diff --git a/test/barrier/barrier.ml b/test/barrier/barrier.ml index 32b2e497..db364004 100644 --- a/test/barrier/barrier.ml +++ b/test/barrier/barrier.ml @@ -1,20 +1,17 @@ type t = { waiters : int Atomic.t; size : int; passed : int Atomic.t } -let create n = { waiters = Atomic.make 0; size = n; passed = Atomic.make 0 } +let create n = { waiters = Atomic.make n; size = n; passed = Atomic.make 0 } let await { waiters; size; passed } = - (* Wait for the barrier to release the previous group *) + if Atomic.fetch_and_add passed 1 = size - 1 then ( + Atomic.set passed 0; + Atomic.set waiters 0); + while Atomic.get waiters = size do Domain.cpu_relax () done; - (* Add itself in the waiters group *) + Atomic.incr waiters; - (* Wait for enough waiters to arrive *) while Atomic.get waiters < size do Domain.cpu_relax () - done; - (* Have passed. Increased [passed]. If last one to pass, reset the - barrier. *) - if Atomic.fetch_and_add passed 1 = size - 1 then ( - Atomic.set passed 0; - Atomic.set waiters 0) + done diff --git a/test/barrier/barrier.mli b/test/barrier/barrier.mli index 58007047..c2092158 100644 --- a/test/barrier/barrier.mli +++ b/test/barrier/barrier.mli @@ -37,6 +37,19 @@ List.iter Domain.join domains ]} + + It also enables to have rounds such as a domain can not begin a new + round before all other domains have finished the previous one. This + can be easily observed by changing the printer function in the + previous example by this one : + + {[ + let printer i () = + Barrier.await barrier; + Format.printf "First round - Domain spawn in %dth position@." i; + Barrier.await barrier; + Format.printf "Second round - Domain spawn in %dth position@." i + ]} *) type t From 057c02be48952426981f95eb4070e8207b7d4e44 Mon Sep 17 00:00:00 2001 From: Sudha Parimala Date: Wed, 13 Sep 2023 13:12:26 +0530 Subject: [PATCH 22/22] Update examples to reflect lockfree -> saturn --- examples/dune | 2 +- examples/michael_scott_queue.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/dune b/examples/dune index f7fe0bbb..f00ad6f1 100644 --- a/examples/dune +++ b/examples/dune @@ -1,3 +1,3 @@ (executables (names michael_scott_queue) - (libraries lockfree)) + (libraries saturn_lockfree)) diff --git a/examples/michael_scott_queue.ml b/examples/michael_scott_queue.ml index 8c4060b9..2e80ed79 100644 --- a/examples/michael_scott_queue.ml +++ b/examples/michael_scott_queue.ml @@ -1,4 +1,4 @@ -open Lockfree.Michael_scott_queue +open Saturn_lockfree.Queue let n_domains = 4