Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.programming.threads > #269 > unrolled thread
| Started by | Masakuni Oishi <yamasa@bsdhouse.org> |
|---|---|
| First post | 2011-06-13 09:40 -0700 |
| Last post | 2011-06-15 02:06 -0700 |
| Articles | 20 on this page of 84 — 6 participants |
Back to article view | Back to comp.programming.threads
questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-13 09:40 -0700
Re: questions about memory_order_seq_cst fence Edek <edek.pienkowski@gmail.com> - 2011-06-13 22:39 +0200
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-14 08:27 -0700
Re: questions about memory_order_seq_cst fence Edek <edek.pienkowski@gmail.com> - 2011-06-16 00:21 +0200
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-15 15:48 -0700
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-16 05:03 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 08:35 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 12:05 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 11:19 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 13:57 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 13:51 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 16:53 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 16:17 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 17:37 +0200
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 08:47 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 16:54 +0100
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 09:01 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 17:07 +0100
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 13:59 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-16 14:32 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-17 08:03 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-17 16:19 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-17 15:40 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-30 14:26 +0200
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-17 15:24 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-18 03:49 -0700
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-18 14:40 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-18 15:46 -0700
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-18 20:27 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-18 21:31 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-18 21:37 -0700
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-20 15:45 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-20 20:05 -0700
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-18 14:06 +0200
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 18:32 +0200
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 15:42 -0700
Re: questions about memory_order_seq_cst fence Edek <edek.pienkowski@gmail.com> - 2011-07-10 19:47 +0200
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 08:51 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 17:23 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 18:49 +0200
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-16 08:51 -0700
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 17:25 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 16:56 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-18 14:28 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-20 09:54 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-20 15:39 +0200
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-22 13:24 +0200
Re: questions about memory_order_seq_cst fence Edek <edek.pienkowski@gmail.com> - 2011-06-16 14:39 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 13:55 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-16 12:03 +0200
Re: questions about memory_order_seq_cst fence Edek <edek.pienkowski@gmail.com> - 2011-07-10 19:10 +0200
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-13 16:00 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-13 23:31 -0700
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-14 08:32 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-14 23:05 +0100
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-14 16:44 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-15 08:34 +0100
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-15 02:11 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-15 15:58 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 08:26 +0100
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-16 05:05 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-16 13:11 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-18 15:42 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-20 09:27 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-20 15:30 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-20 15:00 +0100
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-21 14:54 +0200
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-21 18:37 +0200
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-21 15:59 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-22 09:01 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-20 15:41 +0100
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-20 23:24 -0700
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-22 10:46 -0700
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-22 11:19 -0700
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-22 11:57 -0700
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-27 14:05 +0200
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-29 16:14 -0700
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-06-24 01:42 -0700
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-06-27 13:24 +0200
Re: questions about memory_order_seq_cst fence Anthony Williams <anthony.ajw@gmail.com> - 2011-07-01 02:25 -0700
Re: questions about memory_order_seq_cst fence Alexander Terekhov <terekhov@web.de> - 2011-07-01 12:48 +0200
Re: questions about memory_order_seq_cst fence Masakuni Oishi <yamasa@bsdhouse.org> - 2011-06-15 01:53 -0700
Re: questions about memory_order_seq_cst fence Joshua Maurice <joshuamaurice@gmail.com> - 2011-06-15 02:57 -0700
Re: questions about memory_order_seq_cst fence "Chris M. Thomasson" <cristom@charter.net> - 2011-06-15 02:06 -0700
Page 2 of 5 — ← Prev page 1 [2] 3 4 5 Next page →
| From | Anthony Williams <anthony.ajw@gmail.com> |
|---|---|
| Date | 2011-06-17 08:03 +0100 |
| Message-ID | <871uyt3pns.fsf@justsoftwaresolutions.co.uk> |
| In reply to | #314 |
Joshua Maurice <joshuamaurice@gmail.com> writes:
> On Jun 16, 1:59 pm, "Chris M. Thomasson" <cris...@charter.net> wrote:
>> "Anthony Williams" <anthony....@gmail.com> wrote in message
>>
>> news:87boxxahfj.fsf@justsoftwaresolutions.co.uk...
>> > Can you give an example of such code, along with reasoning based on the
>> > C++0x memory model to show that it is not broken?
>>
>> No. Quite frankly, it makes me want to use `std::memory_order_relaxed'
>> everywhere; ordering is provided by `std::atomic_thread_fence(...)'.
>>
>> This better fuc%ing work!
>> _________________________________________________________
>> static std::atomic<int> g_var_1(0);
>> static std::atomic<int> g_var_2(0);
>> static std::atomic<int> g_sync(0);
>>
>> void only_single_producer_in_process_lifetime()
>> {
>> g_var_1.store(1, std::memory_order_relaxed);
>> g_var_2.store(3, std::memory_order_relaxed);
>> std::atomic_thread_fence(std::memory_order_seq_cst);
>> g_sync.store(1, std::memory_order_relaxed);
>>
>> }
>>
>> void many_consumers_in_process_lifetime()
>> {
>> while (! g_sync.load(std::memory_order_relaxed)) BACKOFF();
>> std::atomic_thread_fence(std::memory_order_seq_cst);
>> int var_1 = var_1.load(std::memory_order_relaxed);
>> int var_2 = var_2.load(std::memory_order_relaxed);
>> ASSERT((var_1 + var_2) == 4);}
>
> AFAIK, the fences don't need to be seq_cst. This all works out with
> just acquire and load fences.
Agreed.
> This is another reason that I'm feeling a little miffed about seq_cst.
> Sometimes seq_cst fences don't need seq_cst reads and writes to be
> more than acq_rel fences. Sometimes they do need seq_cst reads and
> writes to be more than acq_rel fences.
True.
> seq_cst fences seem to give no guarantees for two non-seq_cst reads.
> At least, seq_cst fences gives no additional guarantees w.r.t. two non-
> seq_cst reads above and beyond the guarantees of acq_rel fences. At
> least, that's what I'm reading now. Considering I only really started
> looking at this the other day, take with great warning please.
You are right, and this is precisely the issue that was the start of
this thread. The concurrency group discussed it. Some of us thought that
SC fences should order relaxed reads, but the final result was that they
don't, as it was too expensive on some architectures (such as IA-64).
Anthony
--
Author of C++ Concurrency in Action http://www.stdthread.co.uk/book/
just::thread C++0x thread library http://www.stdthread.co.uk
Just Software Solutions Ltd http://www.justsoftwaresolutions.co.uk
15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976
[toc] | [prev] | [next] | [standalone]
| From | Alexander Terekhov <terekhov@web.de> |
|---|---|
| Date | 2011-06-17 16:19 +0200 |
| Message-ID | <4DFB6257.8C513BD7@web.de> |
| In reply to | #317 |
Anthony Williams wrote: [...] > SC fences should order relaxed reads, but the final result was that they > don't, as it was too expensive on some architectures (such as IA-64). Care to elaborate? What is the problem regarding IA-64? Refs: http://www.decadent.org.uk/pipermail/cpp-threads/2008-December/001932.html http://www.decadent.org.uk/pipermail/cpp-threads/2008-December/001942.html http://www.decadent.org.uk/pipermail/cpp-threads/2008-December/001954.html regards, alexander.
[toc] | [prev] | [next] | [standalone]
| From | Anthony Williams <anthony.ajw@gmail.com> |
|---|---|
| Date | 2011-06-17 15:40 +0100 |
| Message-ID | <87wrgk34ip.fsf@justsoftwaresolutions.co.uk> |
| In reply to | #318 |
Alexander Terekhov <terekhov@web.de> writes: > Anthony Williams wrote: > [...] >> SC fences should order relaxed reads, but the final result was that they >> don't, as it was too expensive on some architectures (such as IA-64). > > Care to elaborate? What is the problem regarding IA-64? I don't remember, and my notes don't say. I think there was some discussion that relaxed loads would have to be more than just a plain LD instruction if SC fences were to order them, but I really don't remember the details, and wasn't privy to the entire discussion anyway. Anthony -- Author of C++ Concurrency in Action http://www.stdthread.co.uk/book/ just::thread C++0x thread library http://www.stdthread.co.uk Just Software Solutions Ltd http://www.justsoftwaresolutions.co.uk 15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976
[toc] | [prev] | [next] | [standalone]
| From | Alexander Terekhov <terekhov@web.de> |
|---|---|
| Date | 2011-06-30 14:26 +0200 |
| Message-ID | <4E0C6B6B.81E28269@web.de> |
| In reply to | #319 |
Anthony Williams wrote: > > Alexander Terekhov <terekhov@web.de> writes: > > > Anthony Williams wrote: > > [...] > >> SC fences should order relaxed reads, but the final result was that they > >> don't, as it was too expensive on some architectures (such as IA-64). > > > > Care to elaborate? What is the problem regarding IA-64? > > I don't remember, and my notes don't say. I think there was some > discussion that relaxed loads would have to be more than just a plain LD > instruction if SC fences were to order them, but I really don't remember > the details, and wasn't privy to the entire discussion anyway. (from the ongoing email discussion regarding http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html ) <Forward Quoted> Hans Boehm wrote: [...] > > [load relaxed] > > > >> The problem with a plain ld is that it can be reordered with other > >> loads from the same location, violating cache coherence. > > > > Do you mean that > > > > (initially: x = 0) > > > > T1: st x = 1; > > T2: r1 = ld x; r2 = ld x; > > > > r1 == 1, r2 == 0 is allowed due to unordered loads? > > > > Well, that's really interesting... > > According to the spec, yes. Whether any implementations allow that, > I do not know. [...] > Memory_order_relaxed indeed appears to be entirely useless on Itanium. [...] > Abbreviating the example, everything is relaxed, except fences are > seq_cst: > > Thread 1: Thread 2: Thread 3: > r3 = y (1) x = 1 r2 = x (1) > fence1 fence2 > r1 = x (0) y = 1 > > We conclude by 29.8p2 that fence2 happens-before fence1. > > Since the initializing write of zero to x precedes the explicit > store to x in modification order, and the thread 3 read of x > sees the later one, so must the thread 1 read of x, so this is > indeed disallowed. > > For the Itanium spec, I'm referring to > http://download.intel.com/design/itanium/downloads/25142901.pdf , > "A Formal Specification of Intel Itanium Processor Family > Memory Ordering", Oct. 2002. > > In the Itanium translation with st, this indeed does not appear > to be enforced. The store to x can occur and become locally > visible before anything else (except the initializing write), > and remotely visible on thread 3 shortly thereafter, without > imposing any constraints on remote visibility at thread 1. And, > in spite of my earlier claim, I think the same issue arises if > we use acquire/release operations on y instead of the fences. > Thus my natural inclination to blame all of our problems on > fences isn't even correct here :-) > > I really need write atomicity in order to get the kinds of > transitivity guarantees I need, and only st.rel provides those. > > This seems to have no impact on RMW operations, since those > become globally visible in a single order, even if they are only > acquire operations. regards, alexander.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-17 15:24 -0700 |
| Message-ID | <9uQKp.19806$F25.16380@newsfe04.iad> |
| In reply to | #317 |
"Anthony Williams" <anthony.ajw@gmail.com> wrote in message news:871uyt3pns.fsf@justsoftwaresolutions.co.uk... > Joshua Maurice <joshuamaurice@gmail.com> writes: > >> On Jun 16, 1:59 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: >>> "Anthony Williams" <anthony....@gmail.com> wrote in message >>> >>> news:87boxxahfj.fsf@justsoftwaresolutions.co.uk... >>> > Can you give an example of such code, along with reasoning based on >>> > the >>> > C++0x memory model to show that it is not broken? >>> >>> No. Quite frankly, it makes me want to use `std::memory_order_relaxed' >>> everywhere; ordering is provided by `std::atomic_thread_fence(...)'. >>> >>> This better fuc%ing work! >>> _________________________________________________________ [...] >> AFAIK, the fences don't need to be seq_cst. This all works out with >> just acquire and load fences. > > Agreed. Here is an example of an algorithm that requires a `StoreLoad' membar, (or something else that guarantees such ordering): http://groups.google.com/group/comp.programming.threads/msg/50ced5527a964ca4 I need to ensure that the atomic store to `waitset::m_waitbit' in `waitset::wait_begin()' and `waitset::wait_try_begin()' are sequentially consistent with the load that are contained within`waitset::signal()' and `waitset::broadcast()'. Basically: __________________________________________________ - I cannot let anything in the "user algorithm" sink below the seq_cst barrier in `waitset::signal()' and `waitset::broadcast()'. - I cannot let anything in the "waitset algorithm" rise above the seq_cst barrier in `waitset::signal()' and `waitset::broadcast()'. - I cannot let anything in the "user algorithm" rise above the seq_cst barrier in `waitset::wait_begin()' and `waitset::wait_try_begin()'. __________________________________________________ I don't think that acq_rel barrier is enough for this because it does not seem as if it's required to generate a `StoreLoad' barrier on a SPARC... Humm... Also, I don't think I need the seq_cst barrier in `waitset::wait_commit()'... FWIW, here is Relacy source code: http://pastebin.com/q9R0sqT7 [...]
[toc] | [prev] | [next] | [standalone]
| From | Joshua Maurice <joshuamaurice@gmail.com> |
|---|---|
| Date | 2011-06-18 03:49 -0700 |
| Message-ID | <2081fd67-f37d-42fa-8c4c-b32c8b683a36@r27g2000prr.googlegroups.com> |
| In reply to | #320 |
On Jun 17, 3:24 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > FWIW, here is Relacy source code: > [...] You know, I really ought to look at this tool. All of the descriptions of it I'm seeing talk about "interleavings", which could explain why it missed the allowed execution which breaks the OP's code. That allowed execution is not a sequentially consistent one. It cannot be expressed as a simple interleaving of instructions. It took me the better part of 2 days of all of my spare time, but I finally managed to do it. I wrote my own little thread tool, based on the C++0x rules as best I can understand them. (Thanks again Anthony!) I had to throw away a day's work as I was taking an approach that would result in too big of a space to be searched, but I managed to make the search space much smaller / the search algorithm much better. When given the OP's code, it finds the allowed execution in a second or so, printing the allowed execution. For funzies, when I ran it against the two code pieces at: http://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_C++0x_atomics.html It found the allowed execution of Bartosz's implementation that allows both threads to get the lock in about a second, and it informs me in about a second that in Dmitriy's implementation there is no allowed execution which has both threads getting the lock. It's really fascinating watching how you can change any one little piece, like making an exchange just a write, and seeing the algorithm fail and an allowed execution printed to the screen. I want to thank you all for this thread again, and bearing with me. I feel as though I have a much better handle on all things C++0x threading related.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-18 14:40 -0700 |
| Message-ID | <nX8Lp.2589$z67.1799@newsfe10.iad> |
| In reply to | #321 |
"Joshua Maurice" <joshuamaurice@gmail.com> wrote in message news:2081fd67-f37d-42fa-8c4c-b32c8b683a36@r27g2000prr.googlegroups.com... On Jun 17, 3:24 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > FWIW, here is Relacy source code: > [...] > You know, I really ought to look at this tool. All of the descriptions > of it I'm seeing talk about "interleavings", which could explain why > it missed the allowed execution which breaks the OP's code. That > allowed execution is not a sequentially consistent one. It cannot be > expressed as a simple interleaving of instructions. You can get the source code for Relacy here: http://www.1024cores.net/home/relacy-race-detector > It took me the better part of 2 days of all of my spare time, but I > finally managed to do it. I wrote my own little thread tool, based on > the C++0x rules as best I can understand them. (Thanks again Anthony!) > I had to throw away a day's work as I was taking an approach that > would result in too big of a space to be searched, but I managed to > make the search space much smaller / the search algorithm much > better. Care to share some code!? ;^) Did you use fibers/user threads to simulate the environment? > When given the OP's code, it finds the allowed execution in a second > or so, printing the allowed execution. Nice. > For funzies, when I ran it against the two code pieces at: > > http://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_C++0x_atomics.html > It found the allowed execution of Bartosz's implementation that allows > both threads to get the lock in about a second, and it informs me in > about a second that in Dmitriy's implementation there is no allowed > execution which has both threads getting the lock. It's really > fascinating watching how you can change any one little piece, like > making an exchange just a write, and seeing the algorithm fail and an > allowed execution printed to the screen. Very nice! > I want to thank you all for this thread again, and bearing with me. I > feel as though I have a much better handle on all things C++0x > threading related.
[toc] | [prev] | [next] | [standalone]
| From | Joshua Maurice <joshuamaurice@gmail.com> |
|---|---|
| Date | 2011-06-18 15:46 -0700 |
| Message-ID | <e69af07a-dd09-4844-96ce-98cc2b94030a@j13g2000pro.googlegroups.com> |
| In reply to | #326 |
On Jun 18, 2:40 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message > > news:2081fd67-f37d-42fa-8c4c-b32c8b683a36@r27g2000prr.googlegroups.com... > On Jun 17, 3:24 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > > FWIW, here is Relacy source code: > > [...] > > > You know, I really ought to look at this tool. All of the descriptions > > of it I'm seeing talk about "interleavings", which could explain why > > it missed the allowed execution which breaks the OP's code. That > > allowed execution is not a sequentially consistent one. It cannot be > > expressed as a simple interleaving of instructions. > > You can get the source code for Relacy here: > > http://www.1024cores.net/home/relacy-race-detector > > > It took me the better part of 2 days of all of my spare time, but I > > finally managed to do it. I wrote my own little thread tool, based on > > the C++0x rules as best I can understand them. (Thanks again Anthony!) > > I had to throw away a day's work as I was taking an approach that > > would result in too big of a space to be searched, but I managed to > > make the search space much smaller / the search algorithm much > > better. > > Care to share some code!? ;^) > > Did you use fibers/user threads to simulate the environment? > > > When given the OP's code, it finds the allowed execution in a second > > or so, printing the allowed execution. > > Nice. > > > For funzies, when I ran it against the two code pieces at: > > >http://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_... > > It found the allowed execution of Bartosz's implementation that allows > > both threads to get the lock in about a second, and it informs me in > > about a second that in Dmitriy's implementation there is no allowed > > execution which has both threads getting the lock. It's really > > fascinating watching how you can change any one little piece, like > > making an exchange just a write, and seeing the algorithm fail and an > > allowed execution printed to the screen. > > Very nice! Let me clean it up a little. It's in a really rough shape right now. How did I do it though? I didn't simulate at all. I fed my program the program fragment in question. To specify the program fragment in question, I need to specify to it: - All the threads (of the thing to be tested), - All the atomic variables, - All the memory operations, including: * isfence or acts on a variable * read only, write only, or read-modify-write, (meaningless for fence), * consume, acquire, release, seq_cst * which thread does the memory action * (optional: enhancing at the moment: for the write, what value does it write) * I lumped the start of thread, end of thread, as memory operations * I lumped the create-and-start thread call, and join thread call, as memory operations - information on sequenced-before for the specified memory operations - TODO dependency-ordered-before information Or most of that. From that, I transitively close the sequenced-before. I iterate over all possible sees pairs - a "sees pair" is a pair of a read and a write (possibly read-modify-writes), where the read loads the value from the write. I iterate over all possible modification orders for all atomic variables. I construct the release sequences, given the above information. I construct the synchronizes with partial order, given the above information. I construct the inter-thread happens before partial order, given the above information. I construct the happens before partial order, given the above information. I iterate over all possible total order S values. I test it against all of the relevant rules of the C++0x which I can find. If that particular set passes, then I save the set, and return satisfiable. If that particular set fails, then I iterate to the next possible set, construct all which needs to be constructed, and test that. Repeat as necessary until I've exhausted all possible sets, and if that happens then return not satisfiable. The key was releasing this particular order for iteration and construction. My first attempt was to just iterate over all possible everythings, which was way too big of a space to examine one by one on available computers. With this order, I can construct several of the pieces of information, such as the happens before partial order, instead of iterating over all possible values. Also, with this order, I can put some of the tests earlier, so I can prune the space early, greatly reducing the actual work the program needs to do. For example, I can test 29.3 p12 right after I construct the release sequences, instead of waiting until the end, thereby preventing wasteful time that would fail a test no matter what. As I said, let me clean it up some, and I'll post the code. Of course, as I just wrote it literally yesterday, I'm sure it's full of bugs. I find one every now and then. Currently, it doesn't even support branching, looping, or anything that's not straight line code. I was thinking if and how I could extend my idea to cover that. That's a next step. I'll do that later, presumably after I post what I have now.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-18 20:27 -0700 |
| Message-ID | <G0eLp.1740$Q35.1361@newsfe13.iad> |
| In reply to | #327 |
"Joshua Maurice" <joshuamaurice@gmail.com> wrote in message news:e69af07a-dd09-4844-96ce-98cc2b94030a@j13g2000pro.googlegroups.com... On Jun 18, 2:40 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message [...] > > > It took me the better part of 2 days of all of my spare time, but I > > > finally managed to do it. I wrote my own little thread tool, based on > > > the C++0x rules as best I can understand them. [...] > > Care to share some code!? ;^) [...] > > Very nice! > Let me clean it up a little. It's in a really rough shape right now. > How did I do it though? I didn't simulate at all. I fed my program the > program fragment in question. To specify the program fragment in > question, I need to specify to it: [...] Clever.
[toc] | [prev] | [next] | [standalone]
| From | Joshua Maurice <joshuamaurice@gmail.com> |
|---|---|
| Date | 2011-06-18 21:31 -0700 |
| Message-ID | <8b0d7fcd-0594-4e56-8906-55a1f161dc03@r33g2000prh.googlegroups.com> |
| In reply to | #327 |
On Jun 18, 3:46 pm, Joshua Maurice <joshuamaur...@gmail.com> wrote: > On Jun 18, 2:40 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > > "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message > > >news:2081fd67-f37d-42fa-8c4c-b32c8b683a36@r27g2000prr.googlegroups.com... > > On Jun 17, 3:24 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > > > FWIW, here is Relacy source code: > > > [...] > > > > You know, I really ought to look at this tool. All of the descriptions > > > of it I'm seeing talk about "interleavings", which could explain why > > > it missed the allowed execution which breaks the OP's code. That > > > allowed execution is not a sequentially consistent one. It cannot be > > > expressed as a simple interleaving of instructions. > > > You can get the source code for Relacy here: > > >http://www.1024cores.net/home/relacy-race-detector > > > > It took me the better part of 2 days of all of my spare time, but I > > > finally managed to do it. I wrote my own little thread tool, based on > > > the C++0x rules as best I can understand them. (Thanks again Anthony!) > > > I had to throw away a day's work as I was taking an approach that > > > would result in too big of a space to be searched, but I managed to > > > make the search space much smaller / the search algorithm much > > > better. > > > Care to share some code!? ;^) > > > Did you use fibers/user threads to simulate the environment? > > > > When given the OP's code, it finds the allowed execution in a second > > > or so, printing the allowed execution. > > > Nice. > > > > For funzies, when I ran it against the two code pieces at: > > > >http://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_... > > > It found the allowed execution of Bartosz's implementation that allows > > > both threads to get the lock in about a second, and it informs me in > > > about a second that in Dmitriy's implementation there is no allowed > > > execution which has both threads getting the lock. It's really > > > fascinating watching how you can change any one little piece, like > > > making an exchange just a write, and seeing the algorithm fail and an > > > allowed execution printed to the screen. > > > Very nice! > > Let me clean it up a little. It's in a really rough shape right now. > > How did I do it though? I didn't simulate at all. I fed my program the > program fragment in question. To specify the program fragment in > question, I need to specify to it: > - All the threads (of the thing to be tested), > - All the atomic variables, > - All the memory operations, including: > * isfence or acts on a variable > * read only, write only, or read-modify-write, (meaningless for > fence), > * consume, acquire, release, seq_cst > * which thread does the memory action > * (optional: enhancing at the moment: for the write, what value does > it write) > * I lumped the start of thread, end of thread, as memory operations > * I lumped the create-and-start thread call, and join thread call, as > memory operations > - information on sequenced-before for the specified memory operations > - TODO dependency-ordered-before information > > Or most of that. > > From that, I transitively close the sequenced-before. > I iterate over all possible sees pairs - a "sees pair" is a pair of a > read and a write (possibly read-modify-writes), where the read loads > the value from the write. > I iterate over all possible modification orders for all atomic > variables. > I construct the release sequences, given the above information. > I construct the synchronizes with partial order, given the above > information. > I construct the inter-thread happens before partial order, given the > above information. > I construct the happens before partial order, given the above > information. > I iterate over all possible total order S values. > > I test it against all of the relevant rules of the C++0x which I can > find. If that particular set passes, then I save the set, and return > satisfiable. If that particular set fails, then I iterate to the next > possible set, construct all which needs to be constructed, and test > that. Repeat as necessary until I've exhausted all possible sets, and > if that happens then return not satisfiable. > > The key was releasing this particular order for iteration and > construction. My first attempt was to just iterate over all possible > everythings, which was way too big of a space to examine one by one on > available computers. With this order, I can construct several of the > pieces of information, such as the happens before partial order, > instead of iterating over all possible values. > > Also, with this order, I can put some of the tests earlier, so I can > prune the space early, greatly reducing the actual work the program > needs to do. For example, I can test 29.3 p12 right after I construct > the release sequences, instead of waiting until the end, thereby > preventing wasteful time that would fail a test no matter what. > > As I said, let me clean it up some, and I'll post the code. Of course, > as I just wrote it literally yesterday, I'm sure it's full of bugs. I > find one every now and then. > > Currently, it doesn't even support branching, looping, or anything > that's not straight line code. I was thinking if and how I could > extend my idea to cover that. That's a next step. I'll do that later, > presumably after I post what I have now. https://www.rapidshare.com/files/1030332591/cpptester.zip Well, there it is, sans makefiles or anything else. It uses just standard C++, so it shouldn't bad at all get it working. Sorry that it's light on instructions, and light on comments. I think that the code style is fairly good (but I'm sure I could refactor to make it look nicer for a week). Tested and built only with msvc, so sorry if there's any cross platform issues, but again it's standard C++ only, so I doubt it. Oh, and I know there's some memory leaks in some of the functions in jjracedetector2.cpp - I don't care enough atm to fix them for a program that is designed to die as soon as it finishes this one job (though it would be easy to fix). As before, I mentioned that I just wrote this literally yesterday, and have done little to no testing, so no correctness guarantees, nor any guarantees that it won't format your hard drive (the proverbial result of undefined behavior).
[toc] | [prev] | [next] | [standalone]
| From | Joshua Maurice <joshuamaurice@gmail.com> |
|---|---|
| Date | 2011-06-18 21:37 -0700 |
| Message-ID | <cdb347b0-b3d8-41e6-a79a-74c0793b815a@s16g2000prf.googlegroups.com> |
| In reply to | #329 |
On Jun 18, 9:31 pm, Joshua Maurice <joshuamaur...@gmail.com> wrote: > On Jun 18, 3:46 pm, Joshua Maurice <joshuamaur...@gmail.com> wrote: > > > > > > > > > > > On Jun 18, 2:40 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > > > "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message > > > >news:2081fd67-f37d-42fa-8c4c-b32c8b683a36@r27g2000prr.googlegroups.com... > > > On Jun 17, 3:24 pm, "Chris M. Thomasson" <cris...@charter.net> wrote: > > > > > FWIW, here is Relacy source code: > > > > [...] > > > > > You know, I really ought to look at this tool. All of the descriptions > > > > of it I'm seeing talk about "interleavings", which could explain why > > > > it missed the allowed execution which breaks the OP's code. That > > > > allowed execution is not a sequentially consistent one. It cannot be > > > > expressed as a simple interleaving of instructions. > > > > You can get the source code for Relacy here: > > > >http://www.1024cores.net/home/relacy-race-detector > > > > > It took me the better part of 2 days of all of my spare time, but I > > > > finally managed to do it. I wrote my own little thread tool, based on > > > > the C++0x rules as best I can understand them. (Thanks again Anthony!) > > > > I had to throw away a day's work as I was taking an approach that > > > > would result in too big of a space to be searched, but I managed to > > > > make the search space much smaller / the search algorithm much > > > > better. > > > > Care to share some code!? ;^) > > > > Did you use fibers/user threads to simulate the environment? > > > > > When given the OP's code, it finds the allowed execution in a second > > > > or so, printing the allowed execution. > > > > Nice. > > > > > For funzies, when I ran it against the two code pieces at: > > > > >http://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_... > > > > It found the allowed execution of Bartosz's implementation that allows > > > > both threads to get the lock in about a second, and it informs me in > > > > about a second that in Dmitriy's implementation there is no allowed > > > > execution which has both threads getting the lock. It's really > > > > fascinating watching how you can change any one little piece, like > > > > making an exchange just a write, and seeing the algorithm fail and an > > > > allowed execution printed to the screen. > > > > Very nice! > > > Let me clean it up a little. It's in a really rough shape right now. > > > How did I do it though? I didn't simulate at all. I fed my program the > > program fragment in question. To specify the program fragment in > > question, I need to specify to it: > > - All the threads (of the thing to be tested), > > - All the atomic variables, > > - All the memory operations, including: > > * isfence or acts on a variable > > * read only, write only, or read-modify-write, (meaningless for > > fence), > > * consume, acquire, release, seq_cst > > * which thread does the memory action > > * (optional: enhancing at the moment: for the write, what value does > > it write) > > * I lumped the start of thread, end of thread, as memory operations > > * I lumped the create-and-start thread call, and join thread call, as > > memory operations > > - information on sequenced-before for the specified memory operations > > - TODO dependency-ordered-before information > > > Or most of that. > > > From that, I transitively close the sequenced-before. > > I iterate over all possible sees pairs - a "sees pair" is a pair of a > > read and a write (possibly read-modify-writes), where the read loads > > the value from the write. > > I iterate over all possible modification orders for all atomic > > variables. > > I construct the release sequences, given the above information. > > I construct the synchronizes with partial order, given the above > > information. > > I construct the inter-thread happens before partial order, given the > > above information. > > I construct the happens before partial order, given the above > > information. > > I iterate over all possible total order S values. > > > I test it against all of the relevant rules of the C++0x which I can > > find. If that particular set passes, then I save the set, and return > > satisfiable. If that particular set fails, then I iterate to the next > > possible set, construct all which needs to be constructed, and test > > that. Repeat as necessary until I've exhausted all possible sets, and > > if that happens then return not satisfiable. > > > The key was releasing this particular order for iteration and > > construction. My first attempt was to just iterate over all possible > > everythings, which was way too big of a space to examine one by one on > > available computers. With this order, I can construct several of the > > pieces of information, such as the happens before partial order, > > instead of iterating over all possible values. > > > Also, with this order, I can put some of the tests earlier, so I can > > prune the space early, greatly reducing the actual work the program > > needs to do. For example, I can test 29.3 p12 right after I construct > > the release sequences, instead of waiting until the end, thereby > > preventing wasteful time that would fail a test no matter what. > > > As I said, let me clean it up some, and I'll post the code. Of course, > > as I just wrote it literally yesterday, I'm sure it's full of bugs. I > > find one every now and then. > > > Currently, it doesn't even support branching, looping, or anything > > that's not straight line code. I was thinking if and how I could > > extend my idea to cover that. That's a next step. I'll do that later, > > presumably after I post what I have now. > > https://www.rapidshare.com/files/1030332591/cpptester.zip > > Well, there it is, sans makefiles or anything else. It uses just > standard C++, so it shouldn't bad at all get it working. Sorry that > it's light on instructions, and light on comments. I think that the > code style is fairly good (but I'm sure I could refactor to make it > look nicer for a week). > > Tested and built only with msvc, so sorry if there's any cross > platform issues, but again it's standard C++ only, so I doubt it. > > Oh, and I know there's some memory leaks in some of the functions in > jjracedetector2.cpp - I don't care enough atm to fix them for a > program that is designed to die as soon as it finishes this one job > (though it would be easy to fix). > > As before, I mentioned that I just wrote this literally yesterday, and > have done little to no testing, so no correctness guarantees, nor any > guarantees that it won't format your hard drive (the proverbial result > of undefined behavior). Oh - just to be clear in case you miss it in the random comment in there, it doesn't support anything to do with dependency ordered before and memory_order_consume (yet). The rest is looking good, I think.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-20 15:45 -0700 |
| Message-ID | <54QLp.11751$x11.9588@newsfe09.iad> |
| In reply to | #330 |
"Joshua Maurice" <joshuamaurice@gmail.com> wrote in message
news:cdb347b0-b3d8-41e6-a79a-74c0793b815a@s16g2000prf.googlegroups.com...
[...]
> Oh - just to be clear in case you miss it in the random comment in
> there, it doesn't support anything to do with dependency ordered
> before and memory_order_consume (yet). The rest is looking good, I
> think.
Looking pretty good! FWIW, this version of Petersons algorithms is reported
to work under your testing framework:
_________________________________________________________
void ChrisImpl()
{
cout << "Testing ChrisImpl..." << endl;
AtomicObj flag0 = jjNewAtomicObj("flag0");
AtomicObj flag1 = jjNewAtomicObj("flag1");
AtomicObj turn = jjNewAtomicObj("turn");
ThreadId tfirst = jjNewThread("tfirst");
ThreadId t0 = jjNewThread("t0");
ThreadId t1 = jjNewThread("t1");
jjStartOfThread("tfirst_start", tfirst);
jjWrite("tfirst_flag0_write_0", jjRelaxed, flag0, 0);
jjWrite("tfirst_flag1_write_0", jjRelaxed, flag1, 0);
jjWrite("tfirst_flag1_write_0", jjRelaxed, turn, 0);
jjStartThreadCall("tfirst_starting_t0", t0);
jjStartThreadCall("tfirst_starting_t1", t1);
jjStartOfThread("t0_start", t0);
jjWrite("t0_flag0_write_1", jjRelaxed, flag0, 1);
jjFence("t0_release_fence", jjRelease);
jjRMW("t0_turn_exchange_1", jjRelaxed, turn, 1);
jjFence("t0_acquire_fence", jjAcquire);
MemoryOp t0_flag1_read = jjRead("t0_flag1_read", jjRelaxed, flag1);
MemoryOp t0_turn_read = jjRead("t0_turn_read", jjRelaxed, turn);
jjStartOfThread("t1_start", t1);
jjWrite("t1_flag1_write_1", jjRelaxed, flag1, 1);
jjFence("t1_release_fence", jjRelease);
jjRMW("t1_turn_exchange_1", jjRelaxed, turn, 0);
jjFence("t1_acquire_fence", jjAcquire);
MemoryOp t1_flag0_read = jjRead("t1_flag0_read", jjRelaxed, flag0);
MemoryOp t1_turn_read = jjRead("t1_turn_read", jjRelaxed, turn);
SatisfiabilityTester& st = jjGetGlobalTester();
//assert thread 0 acquires the lock
st.addGenericUserConstraintAtSees(
new OrConstraint(
new ConstrainSeesValue(t0_flag1_read, 0),
new ConstrainSeesValue(t0_turn_read, 0)
));
//assert thread 1 acquires the lock
st.addGenericUserConstraintAtSees(
new OrConstraint(
new ConstrainSeesValue(t1_flag0_read, 0),
new ConstrainSeesValue(t1_turn_read, 1)
));
bool const satisfiable = st.isSatisfiable(); //expected possible
if (satisfiable)
{ cout << "ChrisImpl: Condition Satisfiable" << endl;
st.printState();
cout << "ChrisImpl: Condition Satisfiable" << endl;
}else
cout << "ChrisImpl: Condition Not satisfiable" << endl;
}
_________________________________________________________
AFAICT, it is "identical" to Dmitriy's impl except I use explicit
`atomic_thread_fence()' instructions, and relaxed for every atomic
operation...
[toc] | [prev] | [next] | [standalone]
| From | Joshua Maurice <joshuamaurice@gmail.com> |
|---|---|
| Date | 2011-06-20 20:05 -0700 |
| Message-ID | <549314b2-63c5-472a-8294-9d401543454a@q14g2000prh.googlegroups.com> |
| In reply to | #337 |
On Jun 20, 3:45 pm, "Chris M. Thomasson" <cris...@charter.net> wrote:
> "Joshua Maurice" <joshuamaur...@gmail.com> wrote in message
>
> news:cdb347b0-b3d8-41e6-a79a-74c0793b815a@s16g2000prf.googlegroups.com...
>
> [...]
>
> > Oh - just to be clear in case you miss it in the random comment in
> > there, it doesn't support anything to do with dependency ordered
> > before and memory_order_consume (yet). The rest is looking good, I
> > think.
>
> Looking pretty good! FWIW, this version of Petersons algorithms is reported
> to work under your testing framework:
> _________________________________________________________
> void ChrisImpl()
> {
> cout << "Testing ChrisImpl..." << endl;
>
> AtomicObj flag0 = jjNewAtomicObj("flag0");
> AtomicObj flag1 = jjNewAtomicObj("flag1");
> AtomicObj turn = jjNewAtomicObj("turn");
>
> ThreadId tfirst = jjNewThread("tfirst");
> ThreadId t0 = jjNewThread("t0");
> ThreadId t1 = jjNewThread("t1");
>
> jjStartOfThread("tfirst_start", tfirst);
> jjWrite("tfirst_flag0_write_0", jjRelaxed, flag0, 0);
> jjWrite("tfirst_flag1_write_0", jjRelaxed, flag1, 0);
> jjWrite("tfirst_flag1_write_0", jjRelaxed, turn, 0);
> jjStartThreadCall("tfirst_starting_t0", t0);
> jjStartThreadCall("tfirst_starting_t1", t1);
>
> jjStartOfThread("t0_start", t0);
> jjWrite("t0_flag0_write_1", jjRelaxed, flag0, 1);
> jjFence("t0_release_fence", jjRelease);
> jjRMW("t0_turn_exchange_1", jjRelaxed, turn, 1);
> jjFence("t0_acquire_fence", jjAcquire);
> MemoryOp t0_flag1_read = jjRead("t0_flag1_read", jjRelaxed, flag1);
> MemoryOp t0_turn_read = jjRead("t0_turn_read", jjRelaxed, turn);
>
> jjStartOfThread("t1_start", t1);
> jjWrite("t1_flag1_write_1", jjRelaxed, flag1, 1);
> jjFence("t1_release_fence", jjRelease);
> jjRMW("t1_turn_exchange_1", jjRelaxed, turn, 0);
> jjFence("t1_acquire_fence", jjAcquire);
> MemoryOp t1_flag0_read = jjRead("t1_flag0_read", jjRelaxed, flag0);
> MemoryOp t1_turn_read = jjRead("t1_turn_read", jjRelaxed, turn);
>
> SatisfiabilityTester& st = jjGetGlobalTester();
>
> //assert thread 0 acquires the lock
> st.addGenericUserConstraintAtSees(
> new OrConstraint(
> new ConstrainSeesValue(t0_flag1_read, 0),
> new ConstrainSeesValue(t0_turn_read, 0)
> ));
>
> //assert thread 1 acquires the lock
> st.addGenericUserConstraintAtSees(
> new OrConstraint(
> new ConstrainSeesValue(t1_flag0_read, 0),
> new ConstrainSeesValue(t1_turn_read, 1)
> ));
>
> bool const satisfiable = st.isSatisfiable(); //expected possible
> if (satisfiable)
> { cout << "ChrisImpl: Condition Satisfiable" << endl;
> st.printState();
> cout << "ChrisImpl: Condition Satisfiable" << endl;
> }else
> cout << "ChrisImpl: Condition Not satisfiable" << endl;}
>
> _________________________________________________________
>
> AFAICT, it is "identical" to Dmitriy's impl except I use explicit
> `atomic_thread_fence()' instructions, and relaxed for every atomic
> operation...
I just added some basic support for branching and such. Basically
label statements, and unconditional branches, and branch if the
previous read is equal to a specified int literal. It's working out
pretty well. Two caveats.
One, I put in a user configurable number which specifies how much
branching complexity should be considered. That is, how many times
shall it allow an execution to execute the same branch before ignoring
any more (taken or not taken, more or less that). So, if you set it
too low, it'll miss allowed executions. Set it too high on a complex
enough piece of code, and it'll run for the age of the universe.
Two. Currently, I tried to test the correct solutions with the
criteria that "not both fail to acquire the lock", but unfortunately
my thing reports that it's possible for both to acquire the lock -
incorrectly so. The printed execution is one where one of the threads
continually loads old values, which is disallowed by 29.3 / 13. I
offer no guarantees that I'll ever make it work, though I'm thinking
about how to now. Maybe something like if it sees a thread with a
sequence of reads without writes to some object at the end of the
execution, and it sees all the reads loading some stale value, and the
number of reads is beyond some configurable amount, then it ignores
that execution...
The old interface without branching is still there. The new one is
build on top of the old one to support branching. The new one with
branching is correct only if you set the branching factor high enough,
whereas the old one has no configurable parameters and is simply
correct (modulo bugs).
I'll probably get around to uploading what I have sometime soon. This
has just been a fun side project for me. It was fun. Not sure if I'll
too much more. Not enough value for me for too much work I suspect to
get anything else working. It's expressive enough to cover all
interesting basic algorithms in C++0x (maybe, I think?), and I'll use
sequentially consistent reasoning for the rest.
[toc] | [prev] | [next] | [standalone]
| From | Alexander Terekhov <terekhov@web.de> |
|---|---|
| Date | 2011-06-18 14:06 +0200 |
| Message-ID | <4DFC94D5.1CCB4B8D@web.de> |
| In reply to | #320 |
"Chris M. Thomasson" wrote: [...] > I don't think that acq_rel barrier is enough for this because it does not > seem as if it's required to generate a `StoreLoad' barrier on a SPARC... I agree that acq_rel fence does not provide `StoreLoad' on SPARC. http://www.decadent.org.uk/pipermail/cpp-threads/2008-December/001949.html regards, alexander.
[toc] | [prev] | [next] | [standalone]
| From | Alexander Terekhov <terekhov@web.de> |
|---|---|
| Date | 2011-06-16 18:32 +0200 |
| Message-ID | <4DFA302D.6D7AB65E@web.de> |
| In reply to | #306 |
Anthony Williams wrote: [...] > For reference, 29.3p8 says: > > [ Note: memory_order_seq_cst ensures sequential consistency only for a > program that is free of data races and uses exclusively > memory_order_seq_cst operations. Any use of weaker ordering will > invalidate this guarantee unless extreme care is used. In particular, This is appalling. regards, alexander.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-16 15:42 -0700 |
| Message-ID | <jFvKp.16186$SG4.5690@newsfe03.iad> |
| In reply to | #311 |
"Alexander Terekhov" <terekhov@web.de> wrote in message news:4DFA302D.6D7AB65E@web.de... > > Anthony Williams wrote: > [...] >> For reference, 29.3p8 says: >> >> [ Note: memory_order_seq_cst ensures sequential consistency only for a >> program that is free of data races and uses exclusively >> memory_order_seq_cst operations. Any use of weaker ordering will >> invalidate this guarantee unless extreme care is used. In particular, > > This is appalling. I really do like the SPARC `MEMBAR' instruction!
[toc] | [prev] | [next] | [standalone]
| From | Edek <edek.pienkowski@gmail.com> |
|---|---|
| Date | 2011-07-10 19:47 +0200 |
| Message-ID | <ivcohe$s90$1@node2.news.atman.pl> |
| In reply to | #311 |
On 06/16/2011 06:32 PM, Alexander Terekhov wrote: > > Anthony Williams wrote: > [...] >> For reference, 29.3p8 says: >> >> [ Note: memory_order_seq_cst ensures sequential consistency only for a >> program that is free of data races and uses exclusively >> memory_order_seq_cst operations. Any use of weaker ordering will >> invalidate this guarantee unless extreme care is used. In particular, > > This is appalling. > > regards, > alexander. This is beautiful. The way I see it, is that seq_cst provides for the default use. All other orderings are supposed to serve dedicated purposes. The bad side effect could be that seq_cst affects everything else including such weird orderings as relaxed, in the sense that they would be required to be heavier than needed. But I understand from your post (5th July) that it still does for Itanium. The point I am trying to make is that the above quote is meant to eliminate this side effect, although it does not succeed in every case. I do not understand why this is a problem; but, well, I do not fully understand why relaxed order is really needed either. Not that I do not see the purpose of relaxed if the compiler does a literal line-to-line translation - then, having a simple store (or load) can be better than that plus some fence, but I see no reason why a compiler (or a future CPU) could not eliminate the overhead. [1] Of course, this is limited to cases where relaxed atomic cannot be replaced by non-atomic data. I think I understand why you say this is appalling. But it looks like a reasonable API contract to me. It does affect ops with a bit less strict memory orderings, but without the above clause it would be worse, not better. Am I missing anything obvious, especially in the space between sequentially ordered and "in reasonable time" operations? Edek [1] Take: line 1: x.store(val, relaxed) line 2: y.store(val, release) Supposing line 1 needs any fence because of the memory model consistency, maybe the fence can be omitted for the particular platform, because line 2 already provides enough ordering to "include" line 1? Including seq_cst in the picture, if my logic is correct, would ruin this.
[toc] | [prev] | [next] | [standalone]
| From | "Chris M. Thomasson" <cristom@charter.net> |
|---|---|
| Date | 2011-06-16 08:51 -0700 |
| Message-ID | <8EpKp.6157$PA5.402@newsfe01.iad> |
| In reply to | #300 |
"Anthony Williams" <anthony.ajw@gmail.com> wrote in message news:87oc1xajr3.fsf@justsoftwaresolutions.co.uk... > Alexander Terekhov <terekhov@web.de> writes: > >> Anthony Williams wrote: >> [...] >>> LOCKed instructions have a total order (7.2.3.8 in my copy of the Intel >>> 64 and IA-32 SDM Vol 3A), so if you use XCHG for stores (as per my blog >>> post) then all processors/threads must agree on the order of the writes. >>> >>> This is the key to SC --- all SC stores must have a single total order >>> which is agreed across all threads. >>> >>> Why do you think this is not enough? >> >> x.store(44, memory_order_relaxed); // or _release >> r1 = y.load(memory_order_seq_cst); >> >> there should be a store-load reordering constraint, just like in >> >> x.store(44, memory_order_seq_cst); >> r1 = y.load(memory_order_relaxed); // or _acquire/_consume > > Why? Can you give an example that would be broken by the lack of such a > constraint, and a reference to the FDIS that guarantees the presence of > that constraint? I think I can see this breaking an SMR implementation in which the author thinks that the seq_cst on the load will prevent it from being hoisted up above the preceding store. I am having some trouble trying to understanding why: x.store(44, memory_order_relaxed); // or _release r1 = y.load(memory_order_seq_cst); would not ensure that the store will be rendered visible before the load is performed... What am I missing here?
[toc] | [prev] | [next] | [standalone]
| From | Anthony Williams <anthony.ajw@gmail.com> |
|---|---|
| Date | 2011-06-16 17:23 +0100 |
| Message-ID | <877h8lago3.fsf@justsoftwaresolutions.co.uk> |
| In reply to | #304 |
"Chris M. Thomasson" <cristom@charter.net> writes: > "Anthony Williams" <anthony.ajw@gmail.com> wrote in message > news:87oc1xajr3.fsf@justsoftwaresolutions.co.uk... >> Alexander Terekhov <terekhov@web.de> writes: >> >>> Anthony Williams wrote: >>> [...] >>>> LOCKed instructions have a total order (7.2.3.8 in my copy of the Intel >>>> 64 and IA-32 SDM Vol 3A), so if you use XCHG for stores (as per my blog >>>> post) then all processors/threads must agree on the order of the writes. >>>> >>>> This is the key to SC --- all SC stores must have a single total order >>>> which is agreed across all threads. >>>> >>>> Why do you think this is not enough? >>> >>> x.store(44, memory_order_relaxed); // or _release >>> r1 = y.load(memory_order_seq_cst); >>> >>> there should be a store-load reordering constraint, just like in >>> >>> x.store(44, memory_order_seq_cst); >>> r1 = y.load(memory_order_relaxed); // or _acquire/_consume >> >> Why? Can you give an example that would be broken by the lack of such a >> constraint, and a reference to the FDIS that guarantees the presence of >> that constraint? > > I think I can see this breaking an SMR implementation in which the author > thinks that the seq_cst on the load will prevent it from being hoisted up > above the preceding store. I am having some trouble trying to understanding > why: > > x.store(44, memory_order_relaxed); // or _release > r1 = y.load(memory_order_seq_cst); > > would not ensure that the store will be rendered visible before the load is > performed... What am I missing here? Where is the guarantee that the store *is* rendered visible? Unless there is a specific guarantee given in the C++0x standard, then there is no such guarantee. An SC load does not add any additional ordering constraints wrt non-SC operations over and above a load-acquire. Anthony -- Author of C++ Concurrency in Action http://www.stdthread.co.uk/book/ just::thread C++0x thread library http://www.stdthread.co.uk Just Software Solutions Ltd http://www.justsoftwaresolutions.co.uk 15 Carrallack Mews, St Just, Cornwall, TR19 7UL, UK. Company No. 5478976
[toc] | [prev] | [next] | [standalone]
| From | Alexander Terekhov <terekhov@web.de> |
|---|---|
| Date | 2011-06-16 18:49 +0200 |
| Message-ID | <4DFA340F.40E46617@web.de> |
| In reply to | #310 |
Anthony Williams wrote: [...] > no such guarantee. An SC load does not add any additional ordering > constraints wrt non-SC operations over and above a load-acquire. Then call it memory_order_seq_cst_as_long_as_you_use_seq_cst_atomics_only and get rid of it being default. regards, alexander.
[toc] | [prev] | [next] | [standalone]
Page 2 of 5 — ← Prev page 1 [2] 3 4 5 Next page →
Back to top | Article view | comp.programming.threads
csiph-web