Dear mailing list,
we would like to include a library and a verification tool in the
openHarmony family. This work is the result of more than 3 years of
research by the concurrency team in the Huawei Dresden Research Center.
In the following, I'll describe how this inclusion could improve the
safety and security of the openHarmony ecosystem.
# Context: Concurrency in system software
We know that exploiting the hardware parallelism provided by multicore
CPUs is a necessary step to achieve performance and competitiveness.
Most software is nowadays multithreaded. That includes the kernel,
services, databases, and the applications.
Concurrent programs are, however, very tricky to get right. The costs
of debugging and performing postmortem analysis is huge in due to the
non-deterministic nature of concurrent executions. In every program
execution, threads interleave in different ways not only producing
(potentially) different outcomes, but also exercising different thread
interactions via shared memory accesses. Within these interactions,
subtle bugs reside, waiting to be triggered. They may cause a variety
of undesirable effects such as crashes, data corruption, and hangs.
The cost of concurrency bugs is specially critical in the kernel and
system libraries, which are the basis for the rest of the ecosystem. In
contrast to sequential code, there is no well-established approach to
test concurrent code at the moment. Often such code is barely tested.
Existing techniques such as formal verification, model checking, and
systematic testing require expertise and seldom belong to the
developer's toolbelt.
# Proposal: a verified synchronization library and a verification tool
We propose to tackle concurrency challenges in system software with
practical verification: a path explored for 3 years in the Huawei
Dresden Research Center, and recognized within Huawei and by the
academic community (eg, see [1,2,3,4]).
To let the developers focus on the software functionality and at the
same time to guarantee correctness of the concurrent portions of the
source code, we suggest the use of two complementary approaches:
1. A battle-proof, extensively tested, and formally verified
library of data structures and synchronizations primitives.
2. Practical tools to support the development of custom
concurrent data structures matching the user's needs.
## Libvsync: verified synchronization primitives and data structures
Our libvsync is such a verified library. Libvsync contains low-level
atomics, synchronization primitives, and several common concurrent data
structures that can be safely used in C/C++ programs on x86, Arm or
RISC-V processors.
Our library has been extensively tested and substantial portions have
been verified with model checkers (see tools below). In particular,
Libvsync has been verified to work on architectures with Weak
Consistency Memory Models such as ARMv7, ARMv8, and RISC-V.
Within Huawei, Libvsync has been extensively deployed, helping products
(including the HongMeng kernel) to better use the available hardware
parallelism and achieve a higher confidence of correctness.
## ASAP: As Safe As Possible
Accompanying the library, we have developed a set of tools to test and
verify it. We would like to opensource Asap: Asap takes a test case of a
concurrent code and, using the opensource model checkers GenMC[7] and
Dartagnan[8], verifies whether the code is safe and live. Asap takes
into account the memory model of the target architecture, which is
configurable and can represent x86, ARMv8, Linux Kernel memory model,
among others.
Moreover, to improve synchronization performance, asap optimizes use of
memory barriers (relaxing them), while guaranteeing the concurrent code
is still correct. A set of elaborated techniques allow Asap to perform
the search for a maximally-relaxed combination of barriers and fences in
a very short time.
Libvsync's CI/CD pipeline runs asap on every code merged into the
library. But Asap is not limited to code inside Libvsync. It has been
also used to verify code from the Linux Kernel[5] and components in
other Huawei operating systems. With Asap we were also able to find
bugs in existing opensource projects such as DPDK buf_ring[9] and CLH
lock in seL4 microkernel[10].
# Benefits of open sourcing Libvsync and Asap
Libvsync and Asap form a strong solution to support development of
high-performant, safe, and scalable system software. They are already
well recognized within Huawei and by the academia and resulted in
several publications.
We believe that Libvsync and Asap can enhance the openHarmony ecosystem.
Libvsync provides the user with off-the-shelf verified, scalable code.
Asap supports the implementation of advanced data structures that safe
and live. As far as we are aware, no other platforms/community includes
equally powerful solutions in their standard ecosystems.
Furthermore, given the large numbers of requests from the academic
community for access to these projects, we think that opening them can
raise the awareness of top-tier researchers to the openHarmony project.
# Request
We kindly ask for your feedback. Would the community be interested in
including Libvsync and Asap as two new projects? If yes, what would be
the process to follow?
Thank you.
Best regards,
-Diogo
# References
- [1] VSync: verification and optimization for synchronization
primitives on weak memory models (Best paper at ASPLOS'20)
https://dl.acm.org/doi/10.1145/3445814.3446748
- [2] Verifying and Optimizing the HMCS Lock for Arm Servers
https://link.springer.com/chapter/10.1007/978-3-030-91014-3_17
- [3] CLoF: Compositional Lock Framework for Multi-level NUMA Systems
SOSP'21 -- https://dl.acm.org/doi/10.1145/3477132.3483557
- [4] BBQ: Block-based Bounded Queue -- USENIX ATC'22
https://www.usenix.org/conference/atc22/presentation/wang-jiawei
- [5] Verifying and Optimizing Compact NUMA-Aware Locks on WMMs
https://arxiv.org/abs/2111.15240
- [7] GenMC: https://github.com/MPI-SWS/genmc
- [8] Dartagnan: https://github.com/hernanponcedeleon/Dat3M
- [9] DPDK bug_ring bug: http://patches.dpdk.org/patch/75983/
- [10] seL4 bug: https://github.com/seL4/seL4/pull/199
