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

Currently we host 3 projects:

• libvsync: libvsync is a C header-only library that contains most essential building blocks for concurrent applications, including atomic operations, synchronization primitives and concurrent data structures. 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: A framework to support the development of reproducible benchmarks.

• VSync: push-button verification and optimization for synchronization primitives on weak memory models --- ASPLOS'21, Oberhauser et al.
• Verifying and Optimizing the HMCS Lock for Arm Servers --- NETYS'21, Oberhauser et al.
• Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models --- Technical report, 2022, Paolillo et al.
• CLoF: A Compositional Lock Framework for Multi-level NUMA Systems --- SOSP'22, Chehab et al.
• BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling --- ATC'22, Wang et al
• BWoS: Formally Verified Block-based Work Stealing for Parallel Processing --- OSDI'23, Wang et al.
• AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM --- ASPLOS'23, Beck et al.

For questions write us an email: vsync AT huawei DOT com

This project is under the support of OpenHarmony Concurrency & Coordination TSG (Technical Support Group), 并发与协同TSG.