package rowex

  1. Overview
  2. Docs
package rowex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Parameter Make.S

type 'a t
type memory
val bind : 'a t -> ('a -> 'b t) -> 'b t
val return : 'a -> 'a t
val atomic_get : memory -> 'a rd Addr.t -> (atomic, 'v) value -> 'v t
val atomic_set : memory -> 'a wr Addr.t -> (atomic, 'v) value -> 'v -> unit t
val persist : memory -> 'a wr Addr.t -> len:int -> unit t

persist addr ~len forces the data to get written out to memory. Even if cache can be used to load some values, persist ensures that the value is really stored persistently into the given destination such as we guarantee data validity despite power failures.

More concretely, it should be (for len <= word_size):

  sfence clwb addr sfence

NOTE: the first sfence is not systematically needed depending on what was done before (and if it's revelant for the current computation regardless the status of the cache). Such disposition is hard to track and we prefer to assume a correct write order than a micro-optimization.

val movnt64 : memory -> dst:'a wr Addr.t -> int -> unit t

movnt64 is a special instruction that:

  • must write bypassing the write cache
  • must not load the page being written to in the cache

The goal here is that the write must be fundamentally persistent, but we tolerate a cache miss if we try to read the modified page. We tolerate this because movnt64 is involved in creating a new node (and therefore a new key insertion) that should not be read anytime soon.

val set_n48_key : memory -> 'a wr Addr.t -> int -> int -> unit t
val fetch_add : memory -> rdwr Addr.t -> (atomic, int) value -> int -> int t
val fetch_or : memory -> rdwr Addr.t -> (atomic, int) value -> int -> int t
val fetch_sub : memory -> rdwr Addr.t -> (atomic, int) value -> int -> int t
val compare_exchange : memory -> ?weak:bool -> rdwr Addr.t -> (atomic, 'a) value -> 'a Atomic.t -> 'a -> bool t
val pause_intrinsic : unit -> unit t

pause_intrinsic provides a hint to the processor that the code sequence is a spin-wait loop. If ROWEX is used in a scheduler offering the Yield directive, it is advisable to use the latter.

val get : memory -> 'a rd Addr.t -> ('t, 'v) value -> 'v t

Allocation and ROWEX

ROWEX's allocation policy is quite simple: the algorithm requests blocks and the implementer can reuse "residual" blocks. The algorithm also informs when a block should no longer be reachable for any new writers. However, these blocks can still safely be used by current readers. The implementer must therefore keep these blocks until the readers active during the collect have completed their tasks.

Finally, the algorithm can also request the deletion of a block it has just allocated. It does this via the delete action, and it is safe to consider the block as available.

val allocate : memory -> kind:[ `Leaf | `Node ] -> ?len:int -> string list -> rdwr Addr.t t
val delete : memory -> _ Addr.t -> int -> unit t
val collect : memory -> _ Addr.t -> len:int -> uid:int -> unit t