Proposal: re-certification for each instruction step

[jeehoonkang]

It is a "call for discussion" for the matter of re-certification.

Currently we allow a thread to take instruction steps as many as it wants, and its promises are re-certified only after all the instruction steps are executed. It basically allows more behaviors, effectively validating more compiler optimizations (e.g. merging a write and a update).

Some people complained that it looks bad, and now we have quite a concrete reason why we don't want it. Consider the following code snippet:

lock(); // implemented w/ acquire CAS to location "l"
x = 1;
unlock(); // implemented as release write to "l"

Here, we want to do some modular reasoning and conclude that x = 1 cannot be promised before the lock is acquired. However, actually it can be, provided that unlock() is called right before lock(), as in the certification you can lock() "l" that is just released by unlock(). This is basically due to the fact that we re-certify the promises only at the end of a tread step, but not every instruction step, e.g. especially right before lock():

// [x = 1] can be promised
unlock();
// not required to re-certify promises here
lock();
x = 1;
unlock();

I believe the benefit of allowing these kind of reasoning is much bigger than the cost of losing some compiler optimizations, which are anyway not performed in the mainstream compilers.

So I propose to revise the promising semantics in such a way that a thread step is really a single instruction step, and the promises are re-certified for each instruction step.

We may need to adjust simulation relations for compiler optimizations, but it should not be a big deal AFAICT. We will see.

[vafeiadis]

I also disliked the multiple thread steps for each machine step approach, but the alternative seems worse. It seems that you will lose read-acquire after write elimination, which is allowed under RA. Moreover, for locks, a clever compiler may want to replace unlock(); lock() by skip.

…

On 26 Jan 2017, at 22:50, Jeehoon Kang ***@***.***> wrote: It is a "call for discussion" for the matter of re-certification. Currently we allow a thread to take instruction steps as many as it wants, and its promises are re-certified only after all the instruction steps are executed. It basically allows more behaviors, effectively validating more compiler optimizations (e.g. merging a write and a update). Some people complained that it looks bad, and now we have quite a concrete reason why we don't want it. Consider the following code snippet: lock(); // implemented w/ acquire CAS to location "l" x = 1; unlock(); // implemented as release write to "l" Here, we want to do some modular reasoning and conclude that x = 1 cannot be promised before the lock is acquired. However, actually it can be, provided that unlock() is called right before lock(), as in the certification you can lock() "l" that is just released by unlock(): // [x = 1] can unlock(); lock(); x = 1; unlock(); I believe the benefit of allowing these kind of reasoning is much bigger than the cost of losing some compiler optimizations, which are anyway not performed in the mainstream compilers. So I propose to revise the promising semantics in such a way that a thread step is really a single instruction step, and the promises are re-certified for each instruction step. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.