Reference counting and multithreading

Stream: general

[Oleg M]

I am sorry if this question appears to be stupid or already answered, but how exactly Lean does reference counting on multithreaded programs? Is it like Koka with atomics? Or there is something else?

[Sebastian Ullrich]

As far as I know Koka did not diverge from Lean 4 in that regard, yes. Objects marked as multi-threaded use acquire/release atomic operations. I don't know any realistic alternative.

[Oleg M]

Okay, I see, thank you!
I am just thinking that there might be another option, maybe with some lock-free approach. I think atomics might slow down things too much.

[Sebastian Ullrich]

Atomics are lock-free. Atomics are how you do lock-free usually.

[Henrik Böving]

Yeah lock free usually means you reduce your state to 64 bit and start having atomic read compare update ops.

[Oleg M]

I see. Thank you for answering.