Concurrency and Parallelism in Lean4

Stream: lean4

[Sofia Rodrigues]

I'm trying to make some code that runs in parallel in Lean4 and I would like to know some things before starting:

• can IO.asTask cause data races if I'm using IO.Ref?
• Are there Atomics like Rust or C++ in Lean4 or IO.Ref?
• Is IO.Ref atomic?

[Mac Malone]

@Felipe GS Some quick answers:

• Yes
• There is docs4#IO.Mutex which works like an IO.Ref, but can be accessed atomically via the aptly named docs4#IO.Mutex.atomically.
• No

[Schrodinger ZHU Yifan]

Is there something similar to OCaml's Atomic.t?

[Sebastian Ullrich]

Mac Malone said:

There is docs4#IO.Mutex

Those docs specifically state that IO.Ref uses atomics!

[Sebastian Ullrich]

Underdefined terms such as "data race" and "atomic" are a bit dangerous to use without further specification. I think the strongest statement we can make about IO.Ref is that its operations are guaranteed to be sequentially consistent (a very strong definition of "data race freedom") but they may not necessarily be implemented as only a single atomic CPU instruction (they do the best they can in a reference-counted object model).

[Siddhartha Gadgil]

As I use IO.Ref quite a bit, could someone clarify when it is unsafe to use but IO.Mutex can be used safely (and how)?

[Sebastian Ullrich]

Unsafe use should, hopefully!, be restricted to unsafe functions. The only difference between the two types is the kind of lock used as (briefly) described in docs4#IO.Mutex. In short, prefer Mutex when you spend more than a trivial amount of time inside the critical section (Ref.modify*/Mutex.atomically*).

[Henrik Böving]

If you want to speak in kernel terms an IO.Ref is a spinlock and a IO.Mutex is a sleep lock I assume?

[Mac Malone]

Sebastian Ullrich said:

Those docs specifically state that IO.Ref uses atomics!

Fair enough! However, when I think of an atomic reference, I think of a reference one can modify (e.g., via modify) without race conditions. From past experience, this is not possible with IO.Ref and that is why IO.Mutex was introduced. If I understand correctly, the atomicity of IO.Ref is for its load and store operations (e.g., set, get) to prevent data corruption (and ensure proper reference counting).

[Sebastian Ullrich]

I've already stated that Ref.modify is (supposed to be) a critical section and what the difference between the two types is, I'm not sure how I can be more clear here. Should there really be a bug, let's file an issue.

[Mac Malone]

@Sebastian Ullrich No, sorry, you were clear! :smile: I was just detailing the difference I observed and why I didn't think of IO.Ref as atomic in my initial answer.