polytypic

Picos — Interoperable effects based concurrency

https://github.com/ocaml-multicore/picos

What is Picos?

• It is an interface:

  Libraries & Applications          '' Schedulers ''

polytypic

Fear the Obj.magic

Let me first quote a paragraph from the Memory Representation of Values (with my emphasis):

Obj is an undocumented module that exposes the internals of the OCaml compiler and runtime. It is very useful for

polytypic

A lock-free starvation avoiding bag

module type Bag = sig
  type 'a t
  val create : unit -> 'a t
  val to_list : 'a t -> 'a list
  type 'a handle
  val add : 'a t -> 'a -> 'a handle
  val remove : 'a t -> 'a handle -> unit

polytypic

Currently OCaml 5 provides a Domain.DLS module for domain-local storage.

Unfortunately,

1. there is no corresponding Thread.TLS for (sys)thread-local storage, and

2. the current implementation of Domain.DLS is not thread-safe.

polytypic

For a long time OCaml has supported lightweight threads exposed via the Thread module. These threads are often called “systhreads”, but I will simply call them “threads” in this post.

The OCaml Stdlib also provides many mutable data structures such as Hashtbl, Queue, and Stack. As the documentation alerts, none of these are thread-safe.

polytypic

A pattern for using GADTs to subset cases

Consider the following straightforward mutable queue implementation using two stacks:

type 'a adt_queue = {
  mutable head : 'a head;
  mutable tail : 'a tail;
}

polytypic

(* 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
   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

polytypic

A generalized approach to turn a functional data structure into a lock-free starvation avoiding data structure

Any functional data structure can be turned into a lock-free data structure by wrapping it inside an Atomic. For example, consider the following set implementation:

module Identity_set : sig
  type 'a t
  val empty : 'a t

polytypic

title
k-CAS for sweat-free concurrent programming

k-CAS for sweat-free concurrent programming

Vesa Karvonen

polytypic

Extending k-CAS with efficient read-only CMP operations

The kcas library currently uses the GKMZ algorithm for Efficient Multi-word Compare and Swap or MCAS aka k-CAS. This is a nearly optimal algorithm for MCAS as it requires only k + 1 CAS operations.

The new library API also provides a transactional API for using the algorithm. For example, suppose one would create the following shared memory locations: