I don't agree with your latest lines, maybe is cause I miss something but...
When analyzing the code the model could distinguish "executors", which cold be goroutines (main - the entry one, g1, g2, etc) or pieces of code under a certain lock variable. If a variable is ONLY accessed by a single "executor" (including locks) then it is race free. Even if this could not give binary answer as in safe/race but something more like safe/risky.../race it would be useful. You might still need annotations to the tool to let you do unsafe stuff, but I'd rather have to say "let me do this I know what I am doing" than run into issues without noticing. Thanks, Jose El martes, 13 de septiembre de 2016, 8:16:14 (UTC+2), Jan Mercl escribió: > > On Tue, Sep 13, 2016 at 7:53 AM josvazg <jos...@gmail.com <javascript:>> > wrote: > > > Why does Go does not have a static race detector? What are the > difficulties? > > For example, the halting problem. Ok, now seriously. > > > If Rust can do it, using its ownership model, Go could have a tool > checking the AST that analyzes variable scopes and checks globals, > variables passed to goroutines and to/from channels. > > > > If one such followed variable is found in any piece of code to be > accessed from more than 2 places and any access is a write, bam! flag that > code with an error. > > I don't speak Rust, but AFAIK, its model of ownership does not provide > static race detecting, but can prove a race cannot happen, ie. no two paths > can concurrently read and write the same data. But a Go program can be > perfectly reasonable and completely race free even if it can be proven by > Rust's model as having a potential for races - assuming the Go program uses > synchronization properly. Proper synchronization avoids races, but it is > not possible in the general case to prove the synchronization is used > properly, because - the halting problem etc. > > OTOH, a program proving that a particular Go program cannot have a race is > IMO possible to write. What I doubt is its value, because Go code which can > be proven race-free is probably only a small subset of Go code people write. > > -- > > -j > -- 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+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
