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
Dear Diogo， Thanks for your proposal，it's a great job，Libvsync and Asap form a strong solution to support development of high-performant, safe, and scalable system software. I think 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. Best regards, -luchenggang
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@openharmony.io 抄送: Chenhaibo(CSI) <hb.chen@huawei.com>; Jianing (OS-LAB) <ning.jia@huawei.com>; Luchenggang <luchenggang@huawei.com>; Fuming (DRC OS Kernel Lab) <ming.fu@huawei.com>; leijitang <leijitang@huawei.com>; liuyutao (C) <liuyutao2@huawei.com>; Hernan Luis Ponce de Leon <hernanl.leon@huawei.com>; Antonio Paolillo <antonio.paolillo@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
participants (3)
-
Diogo Behrens -
Luchenggang -
luchenggang＠huawei.com