Messages in this thread | | | Subject | Re: [PATCH v2 0/2] Refactor snapshot vs nocow writers locking | From | Valentin Schneider <> | Date | Mon, 29 Jul 2019 17:32:12 +0100 |
| |
On 29/07/2019 16:33, Catalin Marinas wrote: [...] >> ---- MODULE specs ---- >> EXTENDS Integers, Sequences, TLC >> >> CONSTANTS >> NR_WRITERS, >> NR_READERS, >> WRITER_TASK, >> READER_TASK >> >> WRITERS == {WRITER_TASK} \X (1..NR_WRITERS) >> READERS == {READER_TASK} \X (1..NR_READERS) >> THREADS == WRITERS \union READERS > > Recommendation: use symbolic values for WRITERS and READERS (defined in > .cfg: e.g. r1, r2, r3, w1, w2, w2). It allows you do to symmetry > optimisations. We've also hit a TLC bug in the past with process values > made up of a Cartesian product (though it may have been fixed since). >
Right, I had forgotten that one:
https://github.com/tlaplus/tlaplus/issues/164
Being very lazy I dislike having to manually input those, but as you say it can't be avoided if we want to use symmetry.
>> macro ReadLock(tid) >> { >> if (lock_state = "idle" \/ lock_state = "read_locked") { >> lock_state := "read_locked"; >> threads[tid] := "read_locked"; >> } else { >> assert lock_state = "write_locked"; >> \* waiting for writers to finish >> threads[tid] := "write_waiting"; >> await lock_state = "" \/ lock_state = "read_locked"; > > lock_state = "idle"? >
Aye, I didn't modify those macros from the original spec.
>> macro WriteLock(tid) >> { >> if (lock_state = "idle" \/ lock_state = "write_locked") { >> lock_state := "write_locked"; >> threads[tid] := "write_locked"; >> } else { >> assert lock_state = "read_locked"; >> \* waiting for readers to finish >> threads[tid] := "read_waiting"; >> await lock_state = "idle" \/ lock_state = "write_locked"; >> }; >> } > > I'd say that's one of the pitfalls of PlusCal. The above is executed > atomically, so you'd have the lock_state read and updated in the same > action. Looking at the C patches, there is an > atomic_read(&lock->readers) followed by a > percpu_counter_inc(&lock->writers). Between these two, you can have > "readers" becoming non-zero via a different CPU. > > My suggestion would be to use procedures with labels to express the > non-atomicity of such sequences. >
Agreed, I've suggested something like this in my reply.
[...]
| |