Skip to content

Commit

Permalink
Upgrade to ocamlformat 0.27.0
Browse files Browse the repository at this point in the history
  • Loading branch information
polytypic committed Dec 16, 2024
1 parent 2d68931 commit 97e6f09
Show file tree
Hide file tree
Showing 16 changed files with 139 additions and 135 deletions.
2 changes: 1 addition & 1 deletion .ocamlformat
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
profile = default
version = 0.26.2
version = 0.27.0

exp-grouping=preserve
10 changes: 5 additions & 5 deletions src/kcas/kcas.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,8 @@ type 'a state = {
}

(** Tagged GADT for representing both the state of MCAS operations and of the
transaction log or splay [tree]. Different subsets of this GADT are used in
different contexts. See the [root], [tree], and [which] existentials. *)
transaction log or splay [tree]. Different subsets of this GADT are used in
different contexts. See the [root], [tree], and [which] existentials. *)
and _ tdt =
| Before : [> `Before ] tdt
(** The result has been determined to be the [before] value.
Expand All @@ -164,15 +164,15 @@ and _ tdt =
mutable rot : rot;
(** [rot] is for Root or Tree.
This field must be first, see [root_as_atomic] and
[tree_as_ref]. *)
This field must be first, see [root_as_atomic] and [tree_as_ref].
*)
timeout : [ `Set | `Unset ] Timeout.t;
mutable mode : Mode.t;
mutable validate_counter : int;
mutable post_commit : Action.t;
}
-> [> `Xt ] tdt
(** The result might not yet have been determined. The [root] either says
(** The result might not yet have been determined. The [root] either says
which it is or points to the root of the transaction log or [tree].
Note that if/when local/stack allocation mode becomes available in
Expand Down
129 changes: 63 additions & 66 deletions src/kcas/kcas.mli

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion src/kcas_data/accumulator_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module type Ops = sig
type ('x, 'fn) fn

val add : ('x, t -> int -> unit) fn
(** [add a n] increments the value of the accumulator [a] by [n]. [add]
(** [add a n] increments the value of the accumulator [a] by [n]. [add]
operations can be performed scalably in parallel. *)

val incr : ('x, t -> unit) fn
Expand Down
4 changes: 2 additions & 2 deletions src/kcas_data/bits.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ val max_0 : int -> int
(** [max_0 n] is equivalent to [Int.max 0 n]. *)

val is_pow_2 : int -> bool
(** [is_pow_2 n] determines [n] is zero or of the form [1 lsl i] for some
[i]. *)
(** [is_pow_2 n] determines [n] is zero or of the form [1 lsl i] for some [i].
*)

val ceil_pow_2_minus_1 : int -> int
val ceil_pow_2 : int -> int
6 changes: 3 additions & 3 deletions src/kcas_data/dllist.mli
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ open Kcas
- The [length] operation is not provided.
- The [set] operation is not provided.
A non-compositional {!take_all} operation is added for {{:
https://en.wikipedia.org/wiki/Privatization_(computer_programming)}privatization}
A non-compositional {!take_all} operation is added for
{{:https://en.wikipedia.org/wiki/Privatization_(computer_programming)}privatization}
as well as conversions to a list of nodes ({!to_nodes_l} and {!to_nodes_r})
and to a list of values ({!to_list_l} and {!to_list_r}).
Expand Down Expand Up @@ -46,7 +46,7 @@ val create : unit -> 'a t

val create_node : 'a -> 'a node
(** [create_node value] creates a new doubly-linked list node that is not in any
list. The node can then e.g. be added to a list using {!move_l} or
list. The node can then e.g. be added to a list using {!move_l} or
{!move_r}. *)

val get : 'a node -> 'a
Expand Down
4 changes: 2 additions & 2 deletions src/kcas_data/dllist_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ module type Ops = sig
(** {3 Moving all nodes between lists} *)

val swap : ('x, 'a t -> 'a t -> unit) fn
(** [swap l1 l2] exchanges the nodes of the doubly-linked lists [l1] and
[l2]. *)
(** [swap l1 l2] exchanges the nodes of the doubly-linked lists [l1] and [l2].
*)

val transfer_l : ('x, 'a t -> 'a t -> unit) fn
(** [transfer_l l1 l2] removes all nodes of [l1] and adds them to the left of
Expand Down
4 changes: 3 additions & 1 deletion src/kcas_data/hashtbl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -495,7 +495,9 @@ let filter_map_inplace fn t =
Kcas.Xt.commit { tx };
Kcas.Xt.commit { tx = Xt.perform_pending t } |> ignore;
(* Fenceless is safe as commit above has fences. *)
match Loc.fenceless_get raised with Done -> () | exn -> raise exn
match Loc.fenceless_get raised with
| Done -> ()
| exn -> raise exn

let stats t =
let length = ref 0 in
Expand Down
35 changes: 18 additions & 17 deletions src/kcas_data/hashtbl.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@ open Kcas
The interface provides a subset of the OCaml [Stdlib.Hashtbl] module with
some changes:
- The functorial interface of the [Stdlib.Hashtbl] is not provided.
Instead the constructor functions, {!create}, {!of_seq}, and {!rebuild},
take an optional [HashedType] module as an argument. By default {!create}
returns a randomized hash table.
- The functorial interface of the [Stdlib.Hashtbl] is not provided. Instead
the constructor functions, {!create}, {!of_seq}, and {!rebuild}, take an
optional [HashedType] module as an argument. By default {!create} returns
a randomized hash table.
- The [add_seq] and [replace_seq] operations are not provided at all.
- Non-instance specific operations related to randomization (e.g.
[randomize], [is_randomized]) are not provided.
Expand All @@ -20,13 +20,13 @@ open Kcas
{!fold}, and {!stats} are not provided.
Please note that the design is intentionally based on [Stdlib.Hashtbl] and
copies its semantics as accurately as possible. Some of the operations come
copies its semantics as accurately as possible. Some of the operations come
with warnings.
The hash table implementation is designed to avoid starvation. Read-only
accesses can generally proceed in parallel without interference. Write
The hash table implementation is designed to avoid starvation. Read-only
accesses can generally proceed in parallel without interference. Write
accesses that do not change the number of bindings can proceed in parallel
as long as they hit different internal buckets. Write accesses that change
as long as they hit different internal buckets. Write accesses that change
the number of bindings use a scalable {!Accumulator} and only make
infrequent random checks to determine whether the hash table should be
resized. *)
Expand Down Expand Up @@ -80,10 +80,10 @@ val of_seq :
('k * 'v) Seq.t ->
('k, 'v) t
(** [of_seq assoc] creates a new hash table from the given association sequence
[assoc]. The associations are added in the same order as they appear in the
[assoc]. The associations are added in the same order as they appear in the
sequence, using {!replace}, which means that if two pairs have the same key,
only the latest one will appear in the table. See {!create} for the
optional arguments.
only the latest one will appear in the table. See {!create} for the optional
arguments.
⚠️ [of_seq (to_seq t)] does not necessarily copy the bindings of a hash table
correctly. *)
Expand All @@ -109,7 +109,7 @@ val find : ('k, 'v) t -> 'k -> 'v

val to_seq : ('k, 'v) t -> ('k * 'v) Seq.t
(** [to_seq t] takes a snapshot of the keys and values in the hash table and
returns them as an association sequence. Bindings of each individual key
returns them as an association sequence. Bindings of each individual key
appear in the sequence in reverse order of their introduction.
⚠️ [of_seq (to_seq t)] does not necessarily copy the bindings of a hash table
Expand All @@ -134,12 +134,12 @@ val rebuild :
(** [rebuild t] returns a copy of the given hash table [t] optionally rehashing
all of the bindings.
See {!create} for descriptions of the optional arguments. Unlike {!create},
See {!create} for descriptions of the optional arguments. Unlike {!create},
[rebuild] uses the given hash table [t] as a template to get defaults for
the optional arguments. *)

val copy : ('k, 'v) t -> ('k, 'v) t
(** [copy t] is equivalent to [rebuild t]. In other words, the returned hash
(** [copy t] is equivalent to [rebuild t]. In other words, the returned hash
table uses the same {!hashed_type} (and other parameters) as the given hash
table [t]. *)

Expand All @@ -148,15 +148,16 @@ val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit

val filter_map_inplace : ('k -> 'v -> 'v option) -> ('k, 'v) t -> unit
(** [filter_map_inplace f t] applies [f] to all bindings in the hash table [t]
and updates each binding depending on the result of [f]. If [f] returns
[None], the binding is discarded. If [f] returns [Some new_value], the
and updates each binding depending on the result of [f]. If [f] returns
[None], the binding is discarded. If [f] returns [Some new_value], the
binding is updated to associate the key to the [new_value].
⚠️ The given [f] may be called multiple times for the same bindings from
multiple domains in parallel. *)

val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
(** [fold f t a] is equivalent to [Seq.fold_left (fun a (k, v) -> f k v a) a (to_seq t)]. *)
(** [fold f t a] is equivalent to
[Seq.fold_left (fun a (k, v) -> f k v a) a (to_seq t)]. *)

val stats : ('a, 'b) t -> Stdlib.Hashtbl.statistics
(** [stats t] returns statistics about the hash table [t]. *)
48 changes: 26 additions & 22 deletions src/kcas_data/kcas_data.mli
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,15 @@
explicitly documented.
The main feature of these data structure implementations is their
compositionality. If your application does not need compositionality, then
compositionality. If your application does not need compositionality, then
other concurrency and parallelism safe data structure libraries may
potentially offer better performance.
But why should you care about composability?
As an example, consider the implementation of a least-recently-used (LRU)
cache or a bounded associative map, but first, let's open the libraries
for convenience:
cache or a bounded associative map, but first, let's open the libraries for
convenience:
{[
open Kcas
Expand All @@ -41,35 +41,38 @@
and a doubly-linked list and keep track of the amount of space in the cache:
{[
type ('k, 'v) cache =
{ space: int Loc.t;
table: ('k, 'k Dllist.node * 'v) Hashtbl.t;
order: 'k Dllist.t }
type ('k, 'v) cache = {
space : int Loc.t;
table : ('k, 'k Dllist.node * 'v) Hashtbl.t;
order : 'k Dllist.t;
}
]}
On a cache lookup the doubly-linked list node corresponding to the accessed
key is moved to the left end of the list:
{[
let get_opt {table; order; _} key =
let get_opt { table; order; _ } key =
Hashtbl.find_opt table key
|> Option.map @@ fun (node, datum) ->
Dllist.move_l node order; datum
Dllist.move_l node order;
datum
]}
On a cache update, in case of overflow, the association corresponding to the
node on the right end of the list is dropped:
{[
let set {table; order; space; _} key datum =
let set { table; order; space; _ } key datum =
let node =
match Hashtbl.find_opt table key with
| None ->
if 0 = Loc.update space (fun n -> max 0 (n-1))
then Dllist.take_opt_r order
|> Option.iter (Hashtbl.remove table);
Dllist.add_l key order
| Some (node, _) -> Dllist.move_l node order; node
if 0 = Loc.update space (fun n -> max 0 (n - 1)) then
Dllist.take_opt_r order |> Option.iter (Hashtbl.remove table);
Dllist.add_l key order
| Some (node, _) ->
Dllist.move_l node order;
node
in
Hashtbl.replace table key (node, datum)
]}
Expand Down Expand Up @@ -98,33 +101,34 @@
operations. For the [get_opt] operation we end up with
{[
let get_opt ~xt {table; order; _} key =
let get_opt ~xt { table; order; _ } key =
Hashtbl.Xt.find_opt ~xt table key
|> Option.map @@ fun (node, datum) ->
Dllist.Xt.move_l ~xt node order; datum
Dllist.Xt.move_l ~xt node order;
datum
]}
and the [set] operation is just as easy to convert to a transactional
version. One way to think about transactions is that they give us back the
version. One way to think about transactions is that they give us back the
ability to compose programs such as the above. *)

(** {1 [Stdlib] style data structures}
The data structures in this section are designed to closely mimic the
corresponding unsynchronized data structures in the OCaml [Stdlib]. Each of
corresponding unsynchronized data structures in the OCaml [Stdlib]. Each of
these provide a non-compositional, but concurrency and parallelism safe,
interface that is close to the [Stdlib] equivalent. Additionally,
interface that is close to the [Stdlib] equivalent. Additionally,
compositional transactional interfaces are provided for some operations.
These implementations will use more space than the corresponding [Stdlib]
data structures. Performance, when accessed concurrently, should be
data structures. Performance, when accessed concurrently, should be
competitive or superior compared to naïve locking. *)

module Hashtbl = Hashtbl
module Queue = Queue
module Stack = Stack

(** {1 Communication and synchronization primitives} *)
(** {1 Communication and synchronization primitives} *)

module Mvar = Mvar
module Promise = Promise
Expand Down
6 changes: 3 additions & 3 deletions src/kcas_data/mvar.mli
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,15 @@ open Kcas
with blocking semantics on both {!take} and {!put}.
{b NOTE}: The current implementation is not guaranteed to be fair or
scalable. In other words, when multiple producers block on {!put} or
scalable. In other words, when multiple producers block on {!put} or
multiple consumers block on {!take} the operations are not queued and it is
possible for a particular producer or consumer to starve. *)

(** {1 Common interface} *)

type !'a t
(** The type of a synchronizing variable that may contain a value of type
['a]. *)
(** The type of a synchronizing variable that may contain a value of type ['a].
*)

val create : 'a option -> 'a t
(** [create x_opt] returns a new synchronizing variable that will either be
Expand Down
2 changes: 1 addition & 1 deletion src/kcas_data/promise.mli
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ open Kcas
(** {1 Common interface} *)

type !+'a t
(** The type of a promise of a value of type ['a]. *)
(** The type of a promise of a value of type ['a]. *)

type !-'a u
(** The type of a resolver of a value of type ['a]. *)
Expand Down
5 changes: 3 additions & 2 deletions src/kcas_data/promise_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ module type Ops = sig

val resolve : ('x, 'a u -> 'a -> unit) fn
(** [resolve u v] resolves the promise corresponding to the resolver [u] to
the value [v]. Any awaiters of the corresponding promise are then
the value [v]. Any awaiters of the corresponding promise are then
unblocked. *)

val await : ('x, 'a t -> 'a) blocking_fn
Expand All @@ -25,7 +25,8 @@ module type Ops = sig
(** {2 Result promises} *)

val await_exn : ('x, 'a or_exn -> 'a) blocking_fn
(** [await_exn t] is equivalent to [match await t with v -> v | exception e -> raise e]. *)
(** [await_exn t] is equivalent to
[match await t with v -> v | exception e -> raise e]. *)

val resolve_ok : ('x, ('a, 'b) result u -> 'a -> unit) fn
(** [resolve_ok u v] is equivalent to [resolve u (Ok v)]. *)
Expand Down
6 changes: 3 additions & 3 deletions src/kcas_data/queue.mli
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ open Kcas
(** First-In First-Out (FIFO) queue.
The interface provides a subset of the OCaml [Stdlib.Queue] module.
[transfer] and [add_seq] are not provided at all. Compositional versions of
[transfer] and [add_seq] are not provided at all. Compositional versions of
{!iter}, {!fold}, {!peek}, {!top}, and {!take} are not provided.
The queue implementation is designed to avoid contention between a producer
and a consumer operating concurrently. The implementation is also designed
to avoid starvation. Performance in most concurrent use cases should be
and a consumer operating concurrently. The implementation is also designed
to avoid starvation. Performance in most concurrent use cases should be
superior to what can be achieved with one or two locks. *)

(** {1 Common interface} *)
Expand Down
2 changes: 1 addition & 1 deletion src/kcas_data/stack.mli
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ open Kcas
(** Last-In First-Out (LIFO) stack.
The interface provides a subset of the OCaml [Stdlib.Stack] module.
[add_seq] is not provided at all. Compositional versions of {!iter},
[add_seq] is not provided at all. Compositional versions of {!iter},
{!fold}, {!pop}, and {!top} are not provided.
The implementation is essentially a
Expand Down
9 changes: 4 additions & 5 deletions test/kcas_data/linearizable_chaining_example.ml
Original file line number Diff line number Diff line change
@@ -1,19 +1,18 @@
(** This demonstrates an approach to composing non-blocking linearizable data
structures inspired by the paper
Concurrent Size
by Gal Sela and Erez Petrank
https://arxiv.org/pdf/2209.07100.pdf
Concurrent Size by Gal Sela and Erez Petrank
https://arxiv.org/pdf/2209.07100.pdf
First a [Hashtbl] is implemented that allows [idempotent_add] and
[idempotent_remove] operations to be specified. The hash table makes sure
[idempotent_remove] operations to be specified. The hash table makes sure
that any operations that might witness the addition or the removal of a key
will perform those operations before returning.
Then a [Hashtbl_with_order] is implemented on top of the [Hashtbl] by
specifying the [idempotent_add] and [idempotent_remove] operation such that
they update a lock-free doubly-linked list to maintain a list of the keys in
the hash table in insertion [order]. In other words, we composed a hash
the hash table in insertion [order]. In other words, we composed a hash
table with a doubly-linked list, both lock-free and linearizable, resulting
in a lock-free linearizable hash table that maintains the insertion order.
Expand Down

0 comments on commit 97e6f09

Please sign in to comment.