And with a more accurate spec (appended at the end of this email):
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val =
Some nitpicking below:
On Mon, Jul 29, 2019 at 03:13:42PM +0100, Valentin Schneider wrote:
> specs.tla:
>
> MODULE specs
> EXTENDS Integers, Sequences, TLC
>
> CONSTANTS
> NR_WRITERS,
> NR_READERS,
> WRITER_TASK,
> READER_TASK
>
> WRITERS == {WRITER_TASK} \X (1..NR_WRI
Hello,
Here is the second version of the DRW lock for btrfs. Main changes from v1:
* Fixed all checkpatch warnings (Andrea Parri)
* Properly call write_unlock in btrfs_drw_try_write_lock (Filipe Manana)
* Comment fix.
* Stress tested it via locktorture. Survived for 8 straight days on a 4 sock
3 matches
Mail list logo
