Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

Add Loom model checking for synchronization primitives

オープン
  • 何か問題がありますか？
#185 コメント 1 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 1 日以内に返信

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
30/100
issue の種類
機能追加
明瞭さ
おおむね明確
活発さ
停滞
技術スタック
rust
領域
backend, testing

調査の方向性

PR 184からリンクされているRwLockの変更にある動作するLoomモデルから始め、既存のユニット、統合、ストレス、マルチスレッドテストのインフラストラクチャを確認します。Loomを採用すべきか、またどの同期内部実装を対象範囲に含めるかを判断します。選択した同期ケースを有界モデルでカバーしつつ、CIの実行を現実的な範囲に保てれば完了です。

索引モデルが issue の本文から書いたものです。

説明

As a library providing several synchronization primitives, Asyncband relies on atomic state transitions, waiter queues, and wake-up handling. Conventional unit and stress tests exercise many concurrent schedules, but they cannot systematically explore every relevant execution ordering. Rare interleavings may therefore hide missed wake-ups, leaked ownership, deadlocks, or invalid state transitions.

Loom provides deterministic model checking for concurrent Rust code. Small, focused models can systematically explore relevant interleavings and validate invariants such as:

  • Readers and writers never holding incompatible ownership
  • Waiter publication racing with lock release without missing a wake-up
  • Cancellation before or after ownership is granted
  • Queue-head cancellation preserving follower progress
  • Atomic upgrade and downgrade transitions
  • Correct memory ordering between lock holders

Loom can only explore concurrency performed through its own instrumented primitives. Every atomic, mutex, thread, cell, or other synchronization operation relevant to a model must therefore use the corresponding Loom type. Any synchronization left using an uninstrumented std type falls outside Loom’s scheduler and reduces the model’s coverage, however, this is for the most part covered by the existing test infrastructure. Asyncband would use conditional compilation to select Loom primitives during model checking and the existing std implementations in normal production builds.

A working draft has been added to the RwLock changes (here), where the previous semaphore-based implementation was replaced with a purpose-built atomic scheduler. The draft model-checks ownership exclusion, waiter publication, cancellation around grant, queue progress, upgrade priority, and downgrade handoff.

If the project decides not to adopt Loom, the draft can be removed from the RwLock PR before merging. If adopted, support can be expanded through separate, individual PRs for other synchronization internals, such as:

  • Semaphore
  • AtomicOptionBox
  • Mutex scheduling
  • Countdown and wait-set primitives
  • Channel state machines

The models should remain small and bounded to keep CI execution practical. Loom would exist only to complement the existing unit, integration, stress, and multithreaded tests.

主要言語
Rust
スター
283
フォーク
49
平均マージ
10時間 58分
マージ済み PR（30日）
37

環境構築

このプロジェクトには開発コンテナ、Dockerfile、コントリビューションガイドがありません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

apache/asyncband のほかの issue

apache/asyncband の issue をすべて見る

似ている issue

Rust の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。