S4C is home to a set of concurrency projects targeting system software.

Projects

  • vatomic: A C/C++ header library of atomics operations, supporting mainstream architectures: ARMv7, ARMv8 (AArch32 and AArch64), RISC-V, and x86_64. The memory ordering guarantees provided by the atomic interface are formally described by the VSync Memory Model (VMM). The C interface is compatible with C99 requiring no compiler extensions. The C++ bindings are compatible with C++11.

  • libvsync: A C header-only library that contains most essential building blocks for concurrent applications, including atomic operations (vatomic), synchronization primitives (eg, spinlocks, condition variable, mutexes) and concurrent data structures (eg, queues, lists, maps). The library has been verified and optimized for Weak Memory Models (WMMs) such as in Arm CPUs.

  • vsyncer: is a toolkit to verify and optimize concurrent C/C++ programs on WMMs, which employs state-of-the-art model checkers Dartagnan and GenMC.

  • benchkit: is a Python framework for building and running reproducible performance benchmarks for system software. It provides a declarative way to define benchmark configurations and parameter spaces, and to execute controlled benchmark campaigns across platforms. benchkit emphasizes experimental rigor (such as environment stabilization, affinity and scheduling control, and structured result collection) to enable fair and repeatable evaluation of synchronization primitives, schedulers, and other system components.

  • Dice: A lightweight, extensible C framework for capturing and distributing execution events in multithreaded programs. Designed for low overhead and high flexibility, Dice enables powerful tooling for runtime monitoring, concurrency testing, and deterministic replay using a modular publish-subscribe (pubsub) architecture.

Publications