^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 1) Lemma 1:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 2) If ps_tq is scheduled, ps_tq_active is 1. ps_tq_int() can be called
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 3) only when ps_tq_active is 1.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 4) Proof: All assignments to ps_tq_active and all scheduling of ps_tq happen
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 5) under ps_spinlock. There are three places where that can happen:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 6) one in ps_set_intr() (A) and two in ps_tq_int() (B and C).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 7) Consider the sequnce of these events. A can not be preceded by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 8) anything except B, since it is under if (!ps_tq_active) under
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 9) ps_spinlock. C is always preceded by B, since we can't reach it
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 10) other than through B and we don't drop ps_spinlock between them.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 11) IOW, the sequence is A?(BA|BC|B)*. OTOH, number of B can not exceed
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 12) the sum of numbers of A and C, since each call of ps_tq_int() is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 13) the result of ps_tq execution. Therefore, the sequence starts with
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 14) A and each B is preceded by either A or C. Moments when we enter
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 15) ps_tq_int() are sandwiched between {A,C} and B in that sequence,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 16) since at any time number of B can not exceed the number of these
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 17) moments which, in turn, can not exceed the number of A and C.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 18) In other words, the sequence of events is (A or C set ps_tq_active to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 19) 1 and schedule ps_tq, ps_tq is executed, ps_tq_int() is entered,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 20) B resets ps_tq_active)*.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 21)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 22)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 23) consider the following area:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 24) * in do_pd_request1(): to calls of pi_do_claimed() and return in
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 25) case when pd_req is NULL.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 26) * in next_request(): to call of do_pd_request1()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 27) * in do_pd_read(): to call of ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 28) * in do_pd_read_start(): to calls of pi_do_claimed(), next_request()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 29) and ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 30) * in do_pd_read_drq(): to calls of pi_do_claimed() and next_request()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 31) * in do_pd_write(): to call of ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 32) * in do_pd_write_start(): to calls of pi_do_claimed(), next_request()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 33) and ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 34) * in do_pd_write_done(): to calls of pi_do_claimed() and next_request()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 35) * in ps_set_intr(): to check for ps_tq_active and to scheduling
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 36) ps_tq if ps_tq_active was 0.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 37) * in ps_tq_int(): from the moment when we get ps_spinlock() to the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 38) return, call of con() or scheduling ps_tq.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 39) * in pi_schedule_claimed() when called from pi_do_claimed() called from
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 40) pd.c, everything until returning 1 or setting or setting ->claim_cont
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 41) on the path that returns 0
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 42) * in pi_do_claimed() when called from pd.c, everything until the call
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 43) of pi_do_claimed() plus the everything until the call of cont() if
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 44) pi_do_claimed() has returned 1.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 45) * in pi_wake_up() called for PIA that belongs to pd.c, everything from
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 46) the moment when pi_spinlock has been acquired.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 47)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 48) Lemma 2:
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 49) 1) at any time at most one thread of execution can be in that area or
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 50) be preempted there.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 51) 2) When there is such a thread, pd_busy is set or pd_lock is held by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 52) that thread.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 53) 3) When there is such a thread, ps_tq_active is 0 or ps_spinlock is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 54) held by that thread.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 55) 4) When there is such a thread, all PIA belonging to pd.c have NULL
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 56) ->claim_cont or pi_spinlock is held by thread in question.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 57)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 58) Proof: consider the first moment when the above is not true.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 59)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 60) (1) can become not true if some thread enters that area while another is there.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 61) a) do_pd_request1() can be called from next_request() or do_pd_request()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 62) In the first case the thread was already in the area. In the second,
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 63) the thread was holding pd_lock and found pd_busy not set, which would
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 64) mean that (2) was already not true.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 65) b) ps_set_intr() and pi_schedule_claimed() can be called only from the
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 66) area.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 67) c) pi_do_claimed() is called by pd.c only from the area.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 68) d) ps_tq_int() can enter the area only when the thread is holding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 69) ps_spinlock and ps_tq_active is 1 (due to Lemma 1). It means that
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 70) (3) was already not true.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 71) e) do_pd_{read,write}* could be called only from the area. The only
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 72) case that needs consideration is call from pi_wake_up() and there
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 73) we would have to be called for the PIA that got ->claimed_cont
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 74) from pd.c. That could happen only if pi_do_claimed() had been
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 75) called from pd.c for that PIA, which happens only for PIA belonging
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 76) to pd.c.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 77) f) pi_wake_up() can enter the area only when the thread is holding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 78) pi_spinlock and ->claimed_cont is non-NULL for PIA belonging to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 79) pd.c. It means that (4) was already not true.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 80)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 81) (2) can become not true only when pd_lock is released by the thread in question.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 82) Indeed, pd_busy is reset only in the area and thread that resets
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 83) it is holding pd_lock. The only place within the area where we
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 84) release pd_lock is in pd_next_buf() (called from within the area).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 85) But that code does not reset pd_busy, so pd_busy would have to be
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 86) 0 when pd_next_buf() had acquired pd_lock. If it become 0 while
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 87) we were acquiring the lock, (1) would be already false, since
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 88) the thread that had reset it would be in the area simulateously.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 89) If it was 0 before we tried to acquire pd_lock, (2) would be
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 90) already false.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 91)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 92) For similar reasons, (3) can become not true only when ps_spinlock is released
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 93) by the thread in question. However, all such places within the area are right
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 94) after resetting ps_tq_active to 0.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 95)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 96) (4) is done the same way - all places where we release pi_spinlock within
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 97) the area are either after resetting ->claimed_cont to NULL while holding
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 98) pi_spinlock, or after not tocuhing ->claimed_cont since acquiring pi_spinlock
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 99) also in the area. The only place where ->claimed_cont is made non-NULL is
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 100) in the area, under pi_spinlock and we do not release it until after leaving
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 101) the area.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 102)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 103) QED.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 104)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 105)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 106) Corollary 1: ps_tq_active can be killed. Indeed, the only place where we
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 107) check its value is in ps_set_intr() and if it had been non-zero at that
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 108) point, we would have violated either (2.1) (if it was set while ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 109) was acquiring ps_spinlock) or (2.3) (if it was set when we started to
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 110) acquire ps_spinlock).
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 111)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 112) Corollary 2: ps_spinlock can be killed. Indeed, Lemma 1 and Lemma 2 show
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 113) that the only possible contention is between scheduling ps_tq followed by
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 114) immediate release of spinlock and beginning of execution of ps_tq on
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 115) another CPU.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 116)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 117) Corollary 3: assignment to pd_busy in do_pd_read_start() and do_pd_write_start()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 118) can be killed. Indeed, we are not holding pd_lock and thus pd_busy is already
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 119) 1 here.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 120)
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 121) Corollary 4: in ps_tq_int() uses of con can be replaced with uses of
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 122) ps_continuation, since the latter is changed only from the area.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 123) We don't need to reset it to NULL, since we are guaranteed that there
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 124) will be a call of ps_set_intr() before we look at ps_continuation again.
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 125) We can remove the check for ps_continuation being NULL for the same
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 126) reason - the value is guaranteed to be set by the last ps_set_intr() and
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 127) we never pass it NULL. Assignements in the beginning of ps_set_intr()
^8f3ce5b39 (kx 2023-10-28 12:00:06 +0300 128) can be taken to callers as long as they remain within the area.
Orange Pi5 kernel
Deprecated Linux kernel 5.10.110 for OrangePi 5/5B/5+ boards
3 Commits
0 Branches
0 Tags