[ANN] Major updates to kcas in 0.1.8 and 0.2.0

I’m happy to announce that the kcas library has received major updates.

What is kcas?

kcas provides an implementation of atomic lock-free multi-word
compare-and-swap (MCAS), which is a powerful tool for designing concurrent

First, kcas now uses a new lock-free algorithm that improves performance of kcas significantly over the previously used algorithm. The new algorithm is provided in kcas version 0.1.8 with an API compatible with previous versions of kcas.

Second, the latest version of kcas, 0.2.0, went through a major API redesign. The same functionality as can be found in previous versions is now available through cleaned-up modules. Additionally, the latest library offers a new transactional API, essentially a basic form of STM or Software Transactional Memory, that can make it significantly easier to program lock-free algorithms.

Third, documentation has also been overhauled and there is now both an introduction to the use of the library as well as a reference manual.

So, click here, check out the new documentation, the new transactional API, and enjoy the performance!

Last, there is still more to come. There are plans to extend the range of the library further via a brand-new algorithm and extended support for transactions.


I recently held a talk on the work:

k-CAS for sweat-free concurrent programming

See the video and slides, including full speaker’s notes.


Looking at your kcas examples, I see that transactions are in monadic style:

let pop_front q =
    get q.front >>= function
    | x :: xs -> set q.front xs >>. x
    | [] -> (
        q.back |> get_as List.rev >>= function
        | [] -> forget
        | x :: xs -> set q.back [] >> set q.front xs >>. x))

But in the code the monad is just a “state” monad for a log. In OCaml, manually using the state monad is syntactically heavy and unpleasant, but it can be reformulated as a reader monad on a mutable data structure:

let pop_front ~log q =
  let open Tx in
  match get ~log q.front with
  | x :: xs -> set ~log q.front xs; x
  | [] ->
    match q.back |> get_as ~log List.rev with
    | [] -> forget ~log
    | x :: xs -> set ~log q.back []; set ~log q.front xs; x

Have you considered this?

Now that log is mutable (instead of a persistent value as in the current implementation), you sometimes need to explicitly copy it for backtracking purpose. In particular Tx has a

try_in op
  (fun exn -> ...)
  (fun res -> ...)

operation that can be rewritten in direct style as

let old_log = copy log in
match op with
| exception exn -> let log = old_log in ...
| res -> ...

(This is a bit more verbose and error-prone if you know that resetting the log on error is always the right default, but it also suggests that this approach gives more control to users and may require less built-in combinators, simplifying the overall design.)


manually using the state monad is syntactically heavy and unpleasant, but it can be reformulated as a reader monad on a mutable data structure … Have you considered this?

No, I haven’t.

Hmm… My first reaction is that I wouldn’t want to expose the log to users as such as to pass around as I fear it might be error prone.

Honestly, I don’t think I spent much time thinking about alternatives and just used binding operators (monad) as those now have support in the language (even if they might not be appreciated by all).

One thing that does come to mind, however, is that using a reader over a mutable, log casn * cass ref -> 'a (edited), might have a performance benefit as likely less allocations are required. The write barrier when updating the log, OTOH, might offset that benefit and more. But I have to try this!

Ideally I’d like to use typed algebraic effects for something like this, but we don’t have those yet.

Now that you mention the reader pattern and direct style, I also wonder whether there might be some way to avoid the monadic clutter altogether. I recall Oleg Kiselyov having a talk on some non-deterministic programming approach that didn’t use monads (maybe based on this paper perhaps). Also, the reader pattern reminds me of the old trick used in my Rea library.


(Note: I used log inspired by the code but this could be just tx or tx_state or tx_ctx, what have you.)
There is a risk of users deliberately “leaking” the log and reusing it in improper ways, but the API would not encourage you to do this. I think that the benefits in convenience would vastly outweigh this cost in practice.

I also wonder whether there might be some way to avoid the monadic clutter altogether.

My proposal doesn’t have any monadic clutter.

Oleg’s approach still uses combinators (you build terms in a computation DSL), so (this is more expressive in general but) the convenience cost is sensibly higher than passing a parameter around.

1 Like

Hmm… Well, leaking the log basically allows to break the algorithm, because the algorithm relies on having freshly allocated (unique) descriptors. The internal state descriptors are also mutable (to allow releasing unused objects after the last CAS). So, allowing to leak the log is strictly unsafe. The alternative of rewriting the log (to (re)allocate descriptors as they must be freshly allocated) would likely be relatively expensive.

I did a quick experiment to use a mutable reader monad type 'a t = casn * cass ref -> 'a and it seems to be a bit slower than the state monad. IOW, the write barriers required to update the cass ref seem to be more expensive than threading the state.

TBH, I think the convenience here is subjective. Personally, I’m quite used to using monads. They are a kind of standard approach for this kind of thing. They also leave more room for the implementation to vary underneath. If you e.g. count the number of words in the two pop_front versions, then the monadic version is shorter, i.e. has fewer words. So, what I mean to say here is not that the monadic version is more convenient, but rather that I can see good arguments both ways. BTW, I kind of like the OCaml binding operators, in spite of some shortcomings, compared to various other notations I’ve used.

However, as the library is still a bit experimental, I wouldn’t mind having both interfaces available for experimentation. The Tx module is quite slim and the explicit ~log passing API would likely also be slim. I’m interested to see whether not having the monad layer at all is enough to outweigh the write barrier costs. It does seem, however, that the explicit log passing approach is unsafe and needs to come with a warning label. At least until we have suitable substructural types.

Addition: Hmm… Perhaps one can make the explicit log passing safer by requiring it to be suitably polymorphic with respect to the log:

module Xt : sig
  type 'x t

  val get : xt:'x t -> 'a Loc.t -> 'a
  val set : xt:'x t -> 'a Loc.t -> 'a -> unit
  val update : xt:'x t -> 'a Loc.t -> ('a -> 'a) -> 'a
  val modify : xt:'x t -> 'a Loc.t -> ('a -> 'a) -> unit
  val exchange : xt:'x t -> 'a Loc.t -> 'a -> 'a

  type 'a xt = { run : 'x. xt:'x t -> 'a }

  val commit : ?backoff:Backoff.t -> ?mode:Mode.t -> 'a xt -> 'a

Draft PR (needs more work).

1 Like

Thanks @gasche for the suggestion! There is now a PR to add a Xt or explicit transaction log passing API to kcas. As a point of interest, it includes an example to implement a transactional lock-free leftist heap (a kind of priority queue) based on a textbook imperative implementation.