The problem emerged from a practical case, but thinking on it resulted more and more theoretical directions.
Typically, the lock-free algorithms do relative simple things in the practice, but their implementation is already not very simple. It has mainly debuggability reasons. However, it shouldn't be so, if there would be a way to construct lock-free algorithms automatically.
Consider we have:
- a (not very big) set of simple atomic operations
- a not lock-free algorithm, which uses exclusively these atomic operations, but itself is not lock-free. We can formally specify:
- what the algorithm does (= how the result depends on the initial state)
- how does it (= essentially the executed operations)
Is it, at least in theory, possible, to construct a lock-free version of the same algorithm algorithmically, if it is possible?
I think, if the answer is "no" in the general case, maybe it can be still possible with an (ideally, not very strict) condition on the algorithms, or on the operations.