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:

polytypic

How can one understand and predict the performance of multicore algorithms?

As a first step, I'd recommend acquiring a basic understanding of the MSI protocol. Modern systems use somewhat more complex protocols, but a basic understanding of MSI should be enough to predict the most important phenomena.

Below is an even further simplified model of shared memory based on the MSI protocol. While the model is not precise, and makes several simplifications not based on actual hardware, it should be accurate enough to predict many

polytypic

// This is a very brief and incomplete sketch of how the technique used in
//
//   Effectful OCaml with Objects and Variants
//   https://github.com/polytypic/rea-ml#effectful-ocaml-with-objects-and-variants
//
// could be translated to F#.  The following F# will likely make more sense after
// reading the introduction that you'll find by following the above link.

[<AutoOpen>]
module Rea =

polytypic

build

polytypic

// Computations with extensible environment, error handling, and asynchronicity

// I recently reviewed some F# code that turned out to be using
//
//   Dependency Interpretation
//   https://fsharpforfunandprofit.com/posts/dependencies-4/
//
// and got thinking about whether one could construct a usable Zio like monad
//
//   https://zio.dev/

polytypic

Learning day: ReDiSL

Logistics team held a "learning day" on Thursday 2021-03-04 where we could spend one full day on a project or tutorial of our choosing. I worked on a little proof-of-concept project I dubbed ReDiSL or Redis DSL. This is a little writeup on the topic.

The motivation for working on the Redis DSL or ReDiSL was that it could make for a nice way to work with Redis especially when one is doing

polytypic

// Below is a simple attempt at using GADTs in Scala based on
//
//   https://github.com/palladin/idris-snippets/blob/master/src/HOAS.idr

object Hoas {
  // With case classes one can directly write down what looks like a GADT:
  sealed trait Expr[A]
  final case class Val[A](value: A) extends Expr[A]
  final case class Bin[A, B, C](bin: (A, B) => C, lhs: Expr[A], rhs: Expr[B])
      extends Expr[C]

polytypic

;; Amateurfunctor optics in 1ML --- WORK-IN-PROGRESS!
;;
;; Background:
;;
;;   https://people.mpi-sws.org/~rossberg/1ml/
;;   http://r6.ca/blog/20120623T104901Z.html
;;
;; Run as:
;;
;;   ./1ml prelude.1ml amateurfunctor-optics.1ml

polytypic

;; Type indexed values in 1ML
;;
;; This is a very simple experiment at encoding type-indexed values in 1ML.
;;
;; Background:
;;
;;   https://people.mpi-sws.org/~rossberg/1ml/
;;   http://repository.readscheme.org/ftp/papers/zheyang-icfp98.pdf
;;
;; Run as: