requirements 더 일반화

[tomtomjhj]

• Use after free in Michael-Scott queue? crossbeam-rs/crossbeam#238 (comment)
• 위의 조건과 ejection 같이 고려할 것

[tomtomjhj]

• 조건: E에서 R(b)라면 E+2 이전에 -D(b)이거나(EBR) E+3 이전에 P(b) (ejection 주의)
• PEBR MSQueue는 아마도 안전: 반례상황이 발생하려면 T1이 node0을 defend했어야 함. 따라서 T1이 eject당해서 제때 CAS를 마무리하지 못하더라도 (E+2이전에 -D(b)를 달성하지 못하더라도) node0은 수집되지 않으므로 T3이 node0에서 use-after-free하지 않음

[tomtomjhj]

이거나가 느낌이 좋지않음

[tomtomjhj]

[tomtomjhj]

TODO

• check Seal paper!!
• implement MSQueue!!!

Definitions

• ⇒: implication
• op1 -> op2: op1 precedes op2 in the epoch consensus diagram
  • op1 -/> op2 := ¬(op1 -> op2)
• op1 --> op2: op1 precedes op1 in the global ordering of operations
  • (op1 -> op2) ⇒ (op1 --> op2)
  • TODO (op1 --> op2) ∨ (op2 --> op1)?
    • op1 --/> op2 := ¬(op1 --> op2) == (op2 --> op1)
  • TODO: does transitivity hold?
  • TODO: prove that PEBR provides this relation by appropriate (RAW) synchronization.
• op(b)@e := G(e) -> op(b) -> G(e+2)
• D(b) is a set of all legal dereference of b.
  • Notation: D(b) -> op' := ∀ op ∈ D(b), op -> op'

EBR

• Objective: D(b) -> F(b)
  • NOTE: not equivalent: F(b) -/> D(b)
• Assumptions:
  • A1: R(b)@E ⇒ G(E+3) -> F(b)
  • A2: U(b) -/> D(b)
  • A3: G(E+2) -/> op ⇔ op -> G(E+3)
    • TODO proof?
• Lemma:
  • L1: U(b) -> G(E+2) ⇒ G(E+2) -> ¬D(b)
    • where G(E+2) -> ¬D(b) := ∀ op ∈ D(b), G(E+2) -/> op
    • by A2
  • L2: G(E+2) -> ¬D(b) ⇒ D(b) -> G(E+3)
    • by A3
• Requirement (safety condition): U(b) -> G(E+2)
  • apply L1: G(E+2) -> ¬D(b)
  • apply L2: D(b) -> G(E+3)
  • apply A1: D(b) -> F(b)

EBR-3 MSQueue is wrong

The same execution but T1 pins at E+1 while T2 pins at E and waits until T1 sets up the 개꿀잼몰카.

PEBR

• Conforming to U(b) -> G(E+2) requirement does guarantee no use-after-free
  as in EBR, but the same algorithm may fail to conform to this condition in
  PEBR because the thread can be ejected before it successfully perform U(b).
  So while the condition looks identical to that of EBR, it's a much tighter
  condition in PEBR.
  • MSQueue example: T1 may not be able to U(b) before G(E+2)
• NOTE: Probably can't prove without transitivity of -->
• assumptions:
  • A2': D(b) --> U(b)
  • A4: (P(b) -> F(b)) ⇒ (~P(b) -> F(b))
    (can be free after release() if protect()'ed)
    • need more clarification?
• Objective: D(b) --> F(b)
  • ∀ op ∈ D(b), op --> F(b)
• Requirement (that can be ∨'ed on top of EBR requirement):
  P(b) -> G(E+3) ∧ U(b) -> ~P(b)
  • D(b) --> ~P(b): by A2' and U(b) --> ~P(b) (by the rhs of requirement)
  • apply the conclusion part of A4 (assumption part of A4 holds by lhs of requirement and A1)
  • NOTE: Can be relaxed more.
    ~P(b)@E' ⇒ U(b) -> G(E'+2) where the P(b) itself can be extended somehow.
• MSQueue:
  • T1 provides the guarantee that U(b) -> ~P(b): the unlinking CAS needs protection.
  • T1 must've protected node0 at the start of the push (P(b)).
• So probably we can't directly compare the versatility of EBR vs PEBR because
  the EBR condition gets tighter in PEBR but PEBR provides another condition.

PEBR paper

HP

HP Requirement for retirement

Remind that it's too strong to support some lists.

EBR

Before this section

EBR Requirement for retirement

• proof of safety

Requirement Lemma

• proof of Lemma
• simple proof of safety of all list algorithms

MSQueue proof

• very short description of MSQueue (with pseudocode?)
• more on pop, counter example where it doesn't satisfy the lemma
  • TODO: is this the only counter example?
• strict proof as illustrated above, TODO: resolve TODOs

PEBR

PEBR Requirement for retirement

• why it's subtle: presence of ejection
• state the requirement and proof
• compare w/ EBR again

Requirement Lemma

• proof
• prove list safety

MSQueue