Googles appar
Huvudmeny

Post a Comment On: cbloom rants

"06-01-12 - On C++ Atomic Fences Part 3"

7 Comments -

1 – 7 of 7
Blogger Brian said...

I think banana with a relaxed fetch_add is actually wrong. I
believe that relacy is just missing the bug because of the way it
works.

You are essentially interested in the execution in which the lock
does the exchange, then the unlock is recorded to do the
fetch_add and read 0, then lock does it's add, fence, double
check, get's stuck waiting, and then finally unlock does is store
release.

The problem is that relacy executes the store statements in
program order (and later adds the additional behaviors) and so
when it gets to the relaxed rmw in the unlock operation relacy
can't make the fetch_add return a count of zero because that
could potentially change the value returned by the already
executed fetch_add in the execution trace (in the lock
fetch_add)... You need to use backtracking based search in your
model checker to make this work..

See this excerpt from an email from Dmitry for a related issue:

>For the simplest example, supposed x=y=0 >initially with the following code:
>T1:
>r1=x.load();
>y.store(1, relaxed);
>
>T2:
>r2=y.load();
>x.store(1,relaxed);
>
>Can it simulate the execution in which r1=r2=1 at
>the end?

It is one of few situations that Relacy can't model. The problem
is that (1) Relacy is based on dynamic verification (it actually
executes the program and can observe only what had actually
happen) and (2) it's executes the program in a sequentially
consistent way and applies possible relaxations afterwards. For
the example you provided it means that when the first load is
executed (either r1 or r2) no stores yet happened, but Relacy
must already return some value and the only value it can return
is 0. However it definitely must model r1==1||r2==1. I was
thinking about how it's possible to model such situation, but did
not find any realistic solution.

June 2, 2012 at 5:15 PM

Blogger Brian said...

BTW. We're working on a tool like Relacy that uses backtracking based search to handle these cases plus partial order reduction to optimize the search.

June 2, 2012 at 5:19 PM

Anonymous Anonymous said...

Hmm, without anything at (*1), what rule prevents the compiler from reordering m_count.fetch_add() past m_state.exchange()?

June 3, 2012 at 5:15 AM

Blogger cbloom said...

@Brian - thanks for the comment. Yeah that makes sense and clears up that false positive from Relacy.

I guess any time you do a relaxed store or RMW you have to be very careful about trusting Relacy. And it's a good reminder to me that Relacy can only give definite negatives, not definite positives.

I'm looking forward to your tool! It is so hard to reason about this stuff that everything is suspect until we have rigorous simulators.

June 3, 2012 at 3:11 PM

Blogger cbloom said...

@Preshing - yeah I definitely think you are right. I'll change the post.

I actually had all the ops on m_count as acq_rels in the original version of this example (http://cbloomrants.blogspot.com/2011/07/07-31-11-example-that-needs-seqcst_31.html) and then kept backing off the constraints to try to find the minimal set and went too far.

(I believe the decrement on m_count can be relaxed, but the increment cannot).

June 3, 2012 at 3:14 PM

Anonymous Anonymous said...

You said:

"a single fence in C++0x doesn't really do what you want. (...) you can't just use a fence as a way to publish and have relaxed loads receive it. You need another fence in the receiving thread, so that the fences can "synchronize with" each other."

I don't think this is a C++0x limitation, I think this is a CPU/compiler/logic reality. In any lockless programming there should be errors on the reader and writer. Looking for these pairs helps to identify the need for less obvious barriers.

April 14, 2013 at 9:52 AM

Blogger cbloom said...

No Bruce, that's exactly the point that the naive reader expects, and therefore is why I wrote this extensive series to clarify the subtle issue. Perhaps the previous two posts in the series are more clear about it.

BTW I don't encourage anyone to spend too much time thinking about these subtle corner cases unless you are obsessive like me. Most people will do better to just stick to the C++0x "rules" and make sure you have good transitive "happens before" relationships.

April 14, 2013 at 10:26 AM

You can use some HTML tags, such as <b>, <i>, <a>

This blog does not allow anonymous comments.

Comment moderation has been enabled. All comments must be approved by the blog author.

You will be asked to sign in after submitting your comment.