Expose asymmetric_light_barrier and add a document

[powergee]

It fixes #55.

[jonhoo]

Hi there! Thanks for taking the time to write this up — this is some great documentation to have, and I agree with your rationale for making this function public!

Just one note about a nuance of the doc, and then I'm happy with it 👍

[jonhoo]

The wording here is a little imprecise for my taste. The current phrasing makes it seem like an acknowledgement is somehow "sent" via a call to asymmetric_light_barrier, but that's not really what happens. My understanding is that the barrier specifically has two side-effects:

1. That the load_ptr on head happens strictly after the call to protect_raw
2. That if another thread exchanges head, and that exchange is not observed by this thread, then the protect_raw must be visible to that other thread (since the exchange must have happened-after our load_ptr, which happened after our protect_raw).

I think it would be good to capture some of that nuance here and/or in the docs for asymmetric_light_barrier.

What do you think?

[powergee]

Thank you for reviewing, and I am sorry for the late reply. 😅

I agree with your point. The current explanation might mislead readers that asymmetric_light_barrier alone somehow prevents reclaimers from freeing the object, which is not true. I think that I have omitted too many details.
The relationship between barriers and validation should be described more clearly.

The main idea that must be expressed would be that asymmetric_light_barrier makes essential happens-before relations to hold. For example, if I model the entire system of Hazard pointers like the following...

procedure Protect(p):
  P1. Announce protection of p.
  P2. Issue a **light** barrier.
  P3. Check if p is not retired. If retired, must retry after reloading the pointer.

procedure Reclaim(p):
  R1. Announce retirement of p.
  R2. Issue a **heavy** barrier.
  R3. Check if p is protected. If protected, retry later.

The semantics of the light and heavy barrier are (-> is happens-before relation):

1. If P2 -> R2, P1 -> R3 (the protection of P1 is visible to R3).
2. If R2 -> P2, R1 -> P3 (the retirement of R1 is visible to P3).
3. P2 ensures P1 -> P2 -> P3 and R2 ensures R1 -> R2 -> R3.

These three lemmas cover the two points you mentioned. With these lemmas, we can show that:

1. If P2 happens before R2, the reclaimer will not free p.
2. If R2 happens before P2, the accessor will not access p.

In either case, use-after-free errors do not occur.

So far, this is what I'm going to describe in a revised version. Please feel free to give comments if you want.

I think I'd be able to push a revised version this week. After the work, I would be happy if you review my PR again!

[jonhoo]

Yes, that looks really good, thanks for diving so deep into it!

[codecov-commenter]

Codecov Report

Merging #56 (7e85d86) into main (6c1842f) will increase coverage by 6.1%.
The diff coverage is 100.0%.

Additional details and impacted files

Files	Coverage Δ
src/domain.rs	94.2% <100.0%> (+2.2%)	⬆️
src/hazard.rs	83.2% <ø> (+5.1%)	⬆️
src/lib.rs	78.1% <100.0%> (+18.3%)	⬆️