About Go 1.19 memory model clarificaitons on atomic operations.

[tapi...@gmail.com]

By the latest version of Go Memory Model article: https://go.dev/ref/mem, will the following program always print 1?

https://go.dev/play/p/RICYGip5y8M

[Axel Wagner]

Why wouldn't it?

If the effect of an atomic operation A is observed by atomic operation B, then A is synchronized before B.

To me, it seems pretty clear that it will. Line 13 is synchronized before line 14, which is synchronized before any load observing its effects (i.e. any execution of line 18 which runs into the branch) - and such a load is synchronized before the load in line 20.

Therefore, the store in Line 13 is synchronized before the load in line 20.

 

On Mon, Aug 15, 2022 at 8:37 AM tapi...@gmail.com <tapi...@gmail.com> wrote:

By the latest version of Go Memory Model article: https://go.dev/ref/mem, will the following program always print 1?

https://go.dev/play/p/RICYGip5y8M

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/4d9b8130-d06c-4519-9b99-d161e922d8f6n%40googlegroups.com.

[Changkun Ou]

I think the new memory model does not guarantee this program always prints 1:

1. There is no synchronization guarantee between line 13 and line 14
as these atomic operations are manipulated on the different memory
locations.
2. It is *not* prohibited for the compiler to switch line 13 and line
14 (as I read from section https://go.dev/ref/mem#badcompiler) because
of the above reason, and also, there is no order between line 13 and
line 20. So this is possible: line 14 < line 18 < line 20 < line 13.
3. Depending on the memory layout of a and b, if they are on the same
cache line, then the program will always print 1.

> To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CAEkBMfHpwchwjAMtXNtpVmhb42Ncw9ENKhz5xH9Sv1z_-DMrRA%40mail.gmail.com.

[Axel Wagner]

On Mon, Aug 15, 2022 at 9:06 AM Changkun Ou <ma...@changkun.de> wrote:

I think the new memory model does not guarantee this program always prints 1:

1. There is no synchronization guarantee between line 13 and line 14
as these atomic operations are manipulated on the different memory
locations.

Yes, there is:

The memory operations in each goroutine must correspond to a correct sequential execution of that goroutine, given the values read from and written to memory. That execution must be consistent with the sequenced before relation, defined as the partial order requirements set out by the Go language specification for Go's control flow constructs as well as the order of evaluation for expressions.

[tapi...@gmail.com]

It would be good if the Memory Model article shows some atomic examples.

[Changkun Ou]

> The memory operations in each goroutine must correspond to a correct sequential execution of that goroutine, given the values read from and written to memory. That execution must be consistent with the sequenced before relation, defined as the partial order requirements set out by the Go language specification for Go's control flow constructs as well as the order of evaluation for expressions.

This rule seems a bit unclear in its wording to me. These questions may occur:
1. What does it mean by "a correct sequential execution"? What defines
correct in this case? Is it implied by the variables' written order?
2. Is the rule applicable to multiple variables by written order or
only on different variables separately?

In lines 13 and 14's goroutine, it seems there is no control flow or
any given language spec required order of execution. The most relaxing
requirement: permit the compiler to switch the statement.

--
Changkun Ou (he/him/his)
München, Deutschland
https://changkun.de/

[tapi...@gmail.com]

I tend to think it should print 1, as well this one: https://go.dev/play/p/bax7CoaSV1d

[Axel Wagner]

On Mon, Aug 15, 2022 at 10:02 AM Changkun Ou <ma...@changkun.de> wrote:

> The memory operations in each goroutine must correspond to a correct sequential execution of that goroutine, given the values read from and written to memory. That execution must be consistent with the sequenced before relation, defined as the partial order requirements set out by the Go language specification for Go's control flow constructs as well as the order of evaluation for expressions.

This rule seems a bit unclear in its wording to me. These questions may occur:
1. What does it mean by "a correct sequential execution"? What defines
correct in this case? Is it implied by the variables' written order? 

2. Is the rule applicable to multiple variables by written order or
only on different variables separately?

I think this is trying to pick nits. The rule seems very clear in its intended outcome: A single goroutine should behave as if executing each statement sequentially, and obeying the spec about order of evaluation within a statement.

Any other reading, to me, is trying to find an ambiguity for the sole sake of finding an ambiguity. Generally, the Go spec and the memory model as well doesn't try to be tricky just to be tricky. It expects the reader to apply a certain amount of common sense and biasing themselves towards the most sensible reading.

[Changkun Ou]

> Any other reading, to me, is trying to find an ambiguity for the sole sake of finding an ambiguity.

A reader does not have to be motivated to find ambiguity. If the
sentence can be interpreted with different meanings, other readers may
perceive it differently. To me, the first read of this sentence is
perceived to be ambiguous regarding a single location or multiple
locations. The posted example discusses a and b as two memory
locations.

Atomic operations on a and b are two different statements. It remains
unclear where exactly is the sentence that tries to say this: atomic
operations on different memory locations obey the program statements
order within a goroutine.

On Mon, Aug 15, 2022 at 10:16 AM Axel Wagner

[Axel Wagner]

If you *want* to read the Memory model that way and write your programs accordingly, you are free to do so.

I think you'll find that consistently applying that logic will make it impossible to write correct concurrent programs sharing memory though.

For example, the section about locks. In that snippet, `l` and `a` are in different memory locations, so under your reading of the memory model, it would be valid to arbitrarily reorder those operations. However

The first call to l.Unlock() (in f) is synchronized before the second call to l.Lock() (in main) returns, which is sequenced before the print.

 

(emphasis mine).

It is unambiguously clear that the memory model makes the assumption that within a single goroutine, execution must be consistent with source-order of statements. Every single section demonstrating synchronization primitives contains at least one occurrence of such an assumption.

I refuse to believe that you even actually believe your supposed interpretation of the memory model yourself. But if you do, fine. You are unnecessarily hamstringing yourself, in my opinion. But that's your prerogative.

[jake...@gmail.com]

On Monday, August 15, 2022 at 5:20:58 AM UTC-4 ma...@changkun.de wrote:

> Any other reading, to me, is trying to find an ambiguity for the sole sake of finding an ambiguity.

A reader does not have to be motivated to find ambiguity. If the
sentence can be interpreted with different meanings, other readers may
perceive it differently. To me, the first read of this sentence is
perceived to be ambiguous regarding a single location or multiple
locations. The posted example discusses a and b as two memory
locations.

Atomic operations on a and b are two different statements. It remains
unclear where exactly is the sentence that tries to say this: atomic
operations on different memory locations obey the program statements
order within a goroutine.

Doesn't the Section on Atomics statement say just that:

The APIs in the sync/atomic package are collectively “atomic operations” that can be used to synchronize the execution of different goroutines. If the effect of an atomic operation A is observed by atomic operation B, then A is synchronized before B. All the atomic operations executed in a program behave as though executed in some sequentially consistent order. 

Is your confusion about the term "observed"?

 

[Axel Wagner]

It doesn't say that the particular sequentially consistent order is in any way related to the source code though.

And yes, that's the source of the argument, as I understand it. That if you write `foo(); bar()`, there is supposedly no guarantee that the call to `bar` happens after `foo` returned.

--

You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/3a266d04-db5c-4e16-bf1e-3ea6c7a98168n%40googlegroups.com.

[Axel Wagner]

(or, to be more precise: That the order of actual execution must not be observably different from `bar` happening after `foo`)

[Ludi Rehak]

The 2nd linked playground program appears to be identical to the program that Russ Cox's memory models part 2 blog opens with:

// Thread 1         // Thread 2 

x = 1;                   while(done == 0) { /* loop */ } 

done = 1;            print(x);

Just substitute "a" for "x", and "b" for "done" and you have recreated the same example. 

According to the blog, if "done" is accessed atomically, then the program is guaranteed to print 1. In eliminating data races, you benefit from the DRF-SC property, and can count on the program producing results as though it executes the source code sequentially, interleaved between the threads.

Note that you don't have to access "x" atomically. It's enough to access "done" atomically to eliminate the race on "x", since its atomic access creates a memory barrier.  

[Andrew Harris]

If it's helpful for anyone -

For a speculative / out-of-order processor, implementing the ISA involves microarchitecture that reorders everything. For loads and stores in particular the strategy can mean something like extremely aggressive reordering when instructions enter the pipeline, and invalidation or flushing later on. Keeping various (documented or undocumented) buffers or caches coherent is costly in pipelines, and there's a range of approaches to implementing pipelines that result in different implications here. With this in mind it's not just the compiler reordering things that is worth worrying about, but also the interaction of reordering schemes, which can become practically inexplicable without some conceptual coordination.

The language memory models really are a response to hardware "innovation". Saying "All the atomic operations executed in a program behave as though executed in some sequentially consistent order." is somewhat declarative. It's not a principle that simply emerges from implementation, but a description of behavior that can be reasoned about, unlike actual implementation.