Thread safety programatic definition for Go

[josvazg]

I am trying to come up with a detailed definition of what a thread safe Go program is (and is not). One that a (go) tool could check by analyzing the code for me.

Here is what I got so far:

• If there are no go statements, then the program is single threaded and thus thread safe. I assume that we are only using go built in concurrency primitives.

Otherwise:

• A program is globals safe if any of this is true:

• There are no global variables.

• Globals are read only.

• Globals are only ever modified by the same goroutine.

• Globals are only accessed under the same mutex.

• A program is thread-safe when it is globals safe AND any of these is also true:

• Goroutines only ever get variables, as arguments or from channels, passed by copy.

• After a reference is passed to another goroutine, the caller/sender goroutine never access that reference again (it transferred “ownership” of it).

• Passed references are only accessed under the same mutex.

Of course, whether it is possible for a tool to check all this rules hold or not is the real work.

But for now I just want to make sure I start with a complete and correct definition of "thread safety in go".

Did I miss any possible source of races here?

Note that this kind of rule analysis is only possible for complete programs, for which we know the whole set of code and can compute all possible goroutine and mutex scopes.

Although my initial goal is for the tool to tell me definite answers (thread safe or not), if that is not possible or too complex, I would also think it's useful to have a tool that highlights risks (you might have not noticed).

That way, you can decide to fix or let them be at development time, BEFORE the dynamic race detector might flag real issues to you, probably already in production!

[chrisst...@gmail.com]

On Sunday, January 1, 2017 at 4:43:32 AM UTC-7, josvazg wrote:

I am trying to come up with a detailed definition of what a thread safe Go program is (and is not). One that a (go) tool could check by analyzing the code for me.

 

Otherwise:

• A program is globals safe if any of this is true:

• There are no global variables.

• Globals are read only.

• Globals are only ever modified by the same goroutine.

• Globals are only accessed under the same mutex.

Hi, creating a list of cases that are either safe or unsafe would be infinite and likely error prone as seen above. For example "Globals are only ever modified by the same goroutine." is not accurate because a read during a write is a data race. I would check out the Go Memory Model[1] to get a precise understanding, while sticking to the simple well defined rule[2] that:

"A data race occurs when two or more goroutines access the same variable concurrently (an access means a READ or a WRITE) and at least one of the accesses is a write."

[1] https://golang.org/ref/mem

[2] https://golang.org/doc/articles/race_detector.html

[Michael Jones]

Josvazg, Your notion of "globals safe" should allow init() functions as safe writers. They are always invoked serially. 

--


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.


For more options, visit https://groups.google.com/d/optout.

[josvazg]

Thanks,

That was very useful, I did slip on the globals definition. And I also kind of overlook init()s running before main().

Although I have to check what happens exactly when a go statement is kicked off on an init() body, will it wait for main()?

Also yes, the bottom line for race free code is no write should happen on a goroutine while at least another goroutine can be accessing that value concurrently (to read or write it).

But starting to think how a tool would check it we know that:

- If there are no go statement there is only 1 thread, then we are safe.

- Variables can only be reachable from more than one goroutine if they:

  A) Were passed (by reference) as argument or via channel.

  B) Are global, and thus reachable from anywhere (if public) or their whole package (if private)

How could a variable be reachable from several goroutines otherwise?

[adon...@google.com]

On Sunday, 1 January 2017 06:43:32 UTC-5, josvazg wrote:

I am trying to come up with a detailed definition of what a thread safe Go program is (and is not). One that a (go) tool could check by analyzing the code for me.

You've set yourself an impossible task.  A function is thread-safe (or concurrency-safe) if calling it concurrently from two or more goroutines does not cause it to behave incorrectly. The problem is that in software, even in the absence of concurrency, no-one can really define what "correctly" means precisely enough for a tool to verify it.

There are static and dynamic tools for detecting concurrency problems, but they make very narrow and precise definitions of "correct".  For example, Go's race detector is a dynamic analysis that reports any data races (concurrent accesses to variables where at least one of the accesses is a write) it finds during execution.  As another example, C++'s Annotalysis is a static checker for a non-standard type system (requiring explicit annotations) that can catch misuse of some common locking patterns.  But even if your code passes these two checks, it may still have data races or other kinds of races, locking problems, deadlocks, or a variety of other concurrency problems, plus all the usual bugs of a single-threaded program.