Dear Diogo,
Thanks for your proposal,it's a great job,I am sure Libvsync and Asap form a strong
solution to support development of high-performant, safe, and scalable system software,
and of course it can enhance the openHarmony ecosystem.
Welcome this work as a new TSG project for Security and Confidential Computing, We'll
have a discussion at the TSG meeting as soon as possible.
Thank you.
(The mailing list often has problems. Members cannot receive emails. I copy them to the
TSG member's mailbox. )
Very meaningful work, please TSG Members take time to give valuable advice, thank you!
非常有意义的工作,请TSG各位老师抽时间给出宝贵意见,谢谢!
-----邮件原件-----
发件人: Diogo Behrens
发送时间: 2023年1月12日 23:03
收件人: scy-tsg(a)openharmony.io
抄送: Chenhaibo(CSI) <hb.chen(a)huawei.com>om>; Jianing (OS-LAB)
<ning.jia(a)huawei.com>om>; Luchenggang <luchenggang(a)huawei.com>om>; Fuming (DRC OS
Kernel Lab) <ming.fu(a)huawei.com>om>; leijitang <leijitang(a)huawei.com>om>; liuyutao
(C) <liuyutao2(a)huawei.com>om>; Hernan Luis Ponce de Leon
<hernanl.leon(a)huawei.com>om>; Antonio Paolillo <antonio.paolillo(a)huawei.com>
主题: [RFC] Inclusion of Libvsync and Asap tool in openHarmony
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