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_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). > 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"? > 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. > macro ReadUnlock(tid) { > if (threads[tid] = "read_locked") { > threads[tid] := "idle"; > if (\A thread \in THREADS: threads[thread] # "read_locked") { > \* we were the last read holder, everyone else should be waiting, > unlock the lock > lock_state := "idle"; > }; > }; > } I'd make this close to the proposed C code with atomic counters. You'd not be able to check each thread atomically in practice anyway. -- Catalin