heap-lang CAS capability

Currently, CAS can be performed on all value type, including pair. But this is not normally what real machine can do.

(However this is prevalent in a lot of simplified models?)

cc @jung

Cc @jjourdan I talked about this with JH in the context of lambda-Rust.

When talking about real machines, we can't stop with CAS. Doing an atomic read or write of a pair is also entirely unrealistic, for the same reason as a CAS of such values is unrealistic. However, heap_lang has no notion of non-atomic reads/writes, so we can't forbid such over-sized atomic reads/writes. IMHO forbidding CASes without forbidding reads/writes is just silly.

I see two options:

• We ignore this, but try to make sure manually that we don't rely on this in our proofs. Probably the ticket lock should be changed to follow this rule.
• We add a notion of non-atomic reads/writes to heap_lang, akin to lambda-Rust, and we rule out atomic accesses to compound values. We would have to be careful not to rule out some cases which actually are realistic and which we are (ab)using currently; namely, CASing from NONE (sugar for inl 0) to SOME v (sugar for inr 0). This is CASing a sum, which in general makes no sense, but in the special case of option usually does make sense since the NONE case can often be encoded without increasing the size of the type, by using an otherwise invalid value (e.g. the bit pattern "all 0" for pointers).

Regarding ticket lock, I think it is hard to be done in a lock-free style. Utilizing existing CAS lock can solve the dilemma. I should see other implementation. Also, it is again the practical problem I am currently fighting with: expressing logical atomicity elegantly.

I think it is somewhat wasting to spend too much time on making heap_lang very realistic. But yes, we should take more care about this assumption of over-sized atomicity.

Regarding ticket lock, I think it is hard to be done in a lock-free style. Utilizing existing CAS lock can solve the dilemma.

Why that? Just allocate two locations, one for the next ticket value and one for the number of the owner of the lock. The algorithm doesn't actually rely on CAS'ing both at the same time. I don't think logical atomicity comes in here at all. (It is of course possible to write a logical atomic spec for the ticket lock, just like it is for the CAS lock. But that's entirely orthogonal to using multi-word CAS.)

BTW, I am not sure I agree with the fact that atomic reads/writes are unrealistic. If you implement the language by representing every non-integer value by a pointer to some location containing the data (which itself is immutable), then atomic read and write can be implemented easily. The real problem is deep comparison of values...

Hm, I see. That could work. Sounds rather strange to a C programmer, but whatever ;)

Just allocate two locations, one for the next ticket value and one for the number of the owner of the lock.

Right ... I was thinking about the lock interface stuff. But it looks not a big problem to paste two ref together.

Which interface...?

I mean the lock interface is about a single l; but we have two locations.

Ah, that. You can change the interface and no longer expose which kind of value is representing a lock, so is_lock would have type val -> iProp -> iProp. This is strictly more general, and just as useful for clients.

Now, internally, you can make that value a pair of two locations.

ticket lock is updated https://gitlab.mpi-sws.org/FP/iris-coq/commit/548a5de9301de732bb11bd7d812fa3bb011b13ba

So, do we want to do anything about the original issue @zhangz brought up, namely heap_lang allowing unrealistic CAS? I think I talked about this with @robbertkrebbers way back when, and we agreed it would be too much of a hassle for too little gain. I still feel the same way, so I tend to close this issue as "WONTFIX".

(Notice that there is an implementation even of the language we gave, it's just wasteful: When allocating something of a type that's larger than a word, allocate some additional space there and put a lock into it. Reading, writing and CASing this location first acquire the lock.)

I think indeed for heap_lang this is just too complicated.

Anyway, the role of heap_lang is not to model any actual programming language, but rather to show that we can do proofs about certain programs. The fact that you can write unrealistic programs is not a problem, IMHO. The only thing which is important is that the program that we write are realistic (i.e., faithfully represents the algorithm we want to prove).

Okay, I will close it for now

Status changed to closed

FWIW: I entirely agree with JH's comment about the role of heap_lang.

mentioned in commit 8111cab0

Mentioned in commit 8111cab0