lkml.org 
[lkml]   [2019]   [Jul]   [29]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    SubjectRe: [PATCH v2 0/2] Refactor snapshot vs nocow writers locking
    From
    Date
    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.

    [...]

    \
     
     \ /
      Last update: 2019-07-29 18:32    [W:6.740 / U:0.016 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site