mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
15 lines
704 B
Plaintext
15 lines
704 B
Plaintext
------------------------------ MODULE PairingStoreConcurrentHarness_BadAtomic ------------------------------
|
|
EXTENDS PairingStoreConcurrentHarness
|
|
|
|
(******************************************************************************
|
|
* BUG: cap check is incorrectly re-evaluated at commit time using current now,
|
|
* but commit does not re-check cap (i.e., no lock).
|
|
*
|
|
* In this model, CommitRequest is identical to the base harness; the "bug" is
|
|
* simply that Begin+Commit are non-atomic.
|
|
*
|
|
* This module exists as a named target for a negative model.
|
|
******************************************************************************)
|
|
|
|
=============================================================================
|