Scholarlink

<p>The <i>futex</i> Linux system call enables implementing performant inter-thread and inter-process synchronisation primitives, such as mutexes and condition variables. However, the futex system call is notoriously difficult to use correctly. An early implementation of futex-based mutexes in the Linux Native POSIX Thread Library suffered from a&#xa0;subtle defect. When teaching about clever futex-based mutex designs that avoid these early shortcomings, we have found that their intricacies are hard to understand and difficult to convey to students. In this case study, we use the Promela modelling language to model a number of futex-based mutex and condition variable implementations, and the Spin model checker to verify safety properties over these models. We show that model checking is effective at confirming known bugs that affected real-world implementations and at confirming that current implementations do indeed behave correctly in multi-threaded environments. We also investigate the effectiveness of symmetry reduction and two memory usage reduction techniques for increasing the scalability of model checking in this domain. The Promela models we have developed are available as open source. They may be useful as teaching material for classes that cover futex-based synchronisation primitives and as a template for performing formal verification on new synchronisation primitive designs.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Analysing futex-based synchronisation primitives using model checking

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年2月13日

查看全文
  • Hugues Evrard,
  • Alastair F. Donaldson

摘要

The futex Linux system call enables implementing performant inter-thread and inter-process synchronisation primitives, such as mutexes and condition variables. However, the futex system call is notoriously difficult to use correctly. An early implementation of futex-based mutexes in the Linux Native POSIX Thread Library suffered from a subtle defect. When teaching about clever futex-based mutex designs that avoid these early shortcomings, we have found that their intricacies are hard to understand and difficult to convey to students. In this case study, we use the Promela modelling language to model a number of futex-based mutex and condition variable implementations, and the Spin model checker to verify safety properties over these models. We show that model checking is effective at confirming known bugs that affected real-world implementations and at confirming that current implementations do indeed behave correctly in multi-threaded environments. We also investigate the effectiveness of symmetry reduction and two memory usage reduction techniques for increasing the scalability of model checking in this domain. The Promela models we have developed are available as open source. They may be useful as teaching material for classes that cover futex-based synchronisation primitives and as a template for performing formal verification on new synchronisation primitive designs.