Dr. Ming Fu

Director of Huawei Fields Lab

Address: Shanghai, China         Email: brightfu.gm AT gmail DOT com


Research

I am interested in industry-oriented research on concurrency verification, weak memory consistency, OS architecture and formal verification of OS.

Here is my CV.

Selected Publications
  1. BWoS: Formally Verified Block-based Work Stealing for Parallel Processing
    Jiawei Wang, Bohdan Trach, Ming Fu*, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig and Haibo Chen. (Slides) The 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23), July 10–12, 2023.

  2. AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM
    Martin Beck, Koustubha Bhat, Lazar Stričević, Geng Chen, Diogo Behrens, Ming Fu*, Viktor Vafeiadis, Haibo Chen and Hermann Härtig. The 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'23), March, 2023.

  3. BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling
    Jiawei Wang, Diogo Behrens, Ming Fu*, Lilith Oberhauser, Jonas Oberhauser, and Jitang Lei, Geng Chen, Hermann Härtig, Haibo Chen. The 2022 USENIX Annual Technical Conference (USENIX ATC'22) , July 11–13, 2022.

  4. Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models
    Antonio Paolillo, Hernán Ponce-de-León, Thomas Haas, Diogo Behrens, Rafael Chehab, Ming Fu, Roland Meyer. Technical note, [arXiv], July 9, 2022.

  5. CLoF: A Compositional Lock Framework for Multi-level NUMA Systems
    Rafael Lourenco de Lima Chehab, Antonio Paolillo, Diogo Behrens, Ming Fu*, Hermann Härtig, Haibo Chen (Talk given by Antonio). The 28th ACM Symposium on Operating Systems Principles (SOSP'21) , October 25-28, 2021.

  6. Verifying and Optimizing the HMCS Lock for Arm Servers
    Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis (Talk given by Jonas).
    The 9th International Conference on Networked Systems (NETYS'21), May, 2021.

  7. VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models
    Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu*, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis (Short talk and Full talk given by Jonas).
    The 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'21, Distinguished Paper Award), April, 2021.

  8. Formalizing SPARCv8 instruction set architecture in Coq
    Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng. Science of Computer Programming , 187: 102371 (2020).

  9. Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System
    Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, Haibo Chen. The 27th ACM Symposium on Operating System Principles (SOSP'19). Deerhurst Resort, Huntsville, Ontario, Canada, October 27-30, 2019.

  10. A Practical Verification Framework for Preemptive OS Kernels
    Fengwei Xu, Ming Fu*, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. Proc. 28th International Conference on Computer Aided Verification (CAV'16), Toronto, Ontario, Canada, pages 59--79, July, 2016.

  11. Practical Tactics for Verifying C Programs in Coq
    Jingyuan Cao, Ming Fu* and Xinyu Feng. Proc. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP'15), Mumbai, India, pages 97--108, January, 2015.

  12. Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
    Hongjin Liang, Xinyu Feng and Ming Fu. (Journal version of POPL'12)
    ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 36, No. 1, Article 3, March 2014.

  13. Applying Mathematical Logic to Create Zero-Defect Software
    Yanni Kouskoulas, Ming Fu, Zhong Shao and Peter Kazanzides.
    JOHNS HOPKINS APL TECHNICAL DIGEST, VOLUME 32, NUMBER 2 (2013).

  14. A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations
    Hongjin Liang, Xinyu Feng, and Ming Fu. Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), Philadelphia, Pennsylvania, USA, pages 455-468, January, 2012.

  15. Reasoning about Optimistic Concurrency Using a Program Logic for History
    Ming Fu, Yong Li, Xinyu Feng, Zhong Shao and Yu Zhang.
    Proc. 21st International Conference on Concurrency Theory (CONCUR'10), Paris, France, pages 388-402, August 2010.

Ming Fu
Last modified: December 11, 2022