Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties

オープン
#109 コメント 1 件 リアクション 0 件 担当者 0 名 GitHub で見る

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

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
25/100
issue の種類
バグ
明瞭さ
説明が足りない
活発さ
停滞
領域
tooling

調査の方向性

Bakery-Boulangerie の仕様と Spec における公平性の仮定を調査します。issue では、これらが不十分だと特定されています。DeadlockFreeStarvationFree に必要な仮定を決定します。両方の活性特性が仕様によって満たされた時点で作業は完了です。

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

説明

I've been defining models as part of work on #107. Currently these properties fail so these specs can only be subject to safety checking. Some fairness assumptions are required for the properties to be satisfied. @muenchnerkindl any idea what those fairness assumptions would be? The one in Spec is insufficient.

主要言語
TLA
スター
1.6k
フォーク
224
平均マージ
7日 16時間
マージ済み PR(30日)
4

コントリビューションガイド

コントリビューションガイドを開く

はじめの一歩

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

tlaplus/Examples のほかの issue

tlaplus/Examples の issue をすべて見る

似ている issue

DevTools の issue をもっと見る

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

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