Stream: Coq devs & plugin devs

Topic: Mutable data structures and concurrency

view this post on Zulip Ali Caglayan (Jun 02 2022 at 12:11):

Following from the discussion yesterday in the call, I came across this SO thread:

Is this basically what PMP's "dirty" labeling is doing. By having a mutable node on the mostly immutable ugraph, we can keep track of divergence in the data structure. My understanding from the SO is that "doing the same work twice" is typically more efficient than coming up with fancy ways to merge diverging graphs.

I could also be completely wrong, but I would like to learn a bit more about this.

view this post on Zulip Pierre-Marie Pédrot (Jun 02 2022 at 12:14):

There is a wealth of lore / design patterns around this topic in the Rust community at large (including research stuff like iris)

view this post on Zulip Pierre-Marie Pédrot (Jun 02 2022 at 12:15):

I find the Rustonomicon to have interesting nuggets of wisdom:

view this post on Zulip Pierre-Marie Pédrot (Jun 02 2022 at 12:15):

(aka "unsafeness in an otherwise semantically sound model")

view this post on Zulip Alexander Gryzlov (Jun 02 2022 at 12:32):

Seems to me the answer at SO is describing spinlocking and lockfree/fine-grained approaches. In general this stuff is very tricky to get right which is why you have a whole field of concurrency verification (of which concurrent separation logics like Iris/FCSL are one of the approaches). From the app programmer's point of view the general consensus is usually to avoid lock-free stuff and just use system-provided locks unless you have some very specific scenarios - typically this involves situations where you need some kind of fair throughput, i.e. roughly speaking, all your threads have to proceed at the same pace, or where you really have to manually minimize the amount of context switches between threads. I think a good high-level introduction into the theory of this stuff is Herlihy, Shavit, [2011] "On the nature of progress"

Last updated: Dec 01 2023 at 07:01 UTC