-
Notifications
You must be signed in to change notification settings - Fork 17.8k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
x/tools/go/analysis: request some form of static thread safety analysis for Go #46788
Comments
The gVisor project has recently created checklocks, a IIRC, the tool is fairly immature, so I don't believe it is full-featured and simplified in places for typical conventions used in gVisor, but I think it provides a good starting point, or potentially could be directly used by other projects. |
This is pretty cool, though two things might be showstoppers for us using it right now.
Are there plans to address these? Also, one suggestion--could there be " // +checklocks: all-guarded-by: mu" that specifies that every field in a struct is guarded by the mutex? |
My plan at the moment is to have an internship project look into lock annotations starting at the beginning of September. It will likely start from checklocks. We would also add support for more code patterns (defer, RWMutex, sync.Locker?). The goal of the project would be to evaluate the ergonomics of the checker in real code. I am also curious if we can mix struct tags and comments. If all goes well, this could turn into a proposal or an experimental tool. No promises, but giving you full transparency that this is on my radar.
This would be a breaking changing. This would require a Go2 proposal. A static analyzer is a much smaller lift.
Embeddings are definitely something that needs more thought. No concrete ideas from me at the moment though.
I don't really see why not. That would just be syntactic sugar. There is also a possibility of trying to capture the "mutex hat" idiom in an annotation. That is more flexible, but it is not clear if users would find this too brittle/confusing. Real code examples would really help here. |
Note that you can get a lot of the benefits of static annotation by switching from type MyStruct struct {
fields chan *myStructFields // 1-buffered
}
func NewMyStruct() *MyStruct {
fields := make(chan *myStructFields, 1)
fields <- &myStructFields{}
return &MyStruct{fields: fields}
}
type myStructFields struct {
field1 int
field2 string
field3 []string
} Then the scope of the fields is more closely tied to the synchronization operations for those fields: func (m *MyStruct) GetField1() int {
return m.field1 // Does not compile — field1 is a member of myStructFields, not MyStruct.
} func (m *MyStruct) GetField1() int {
fields := <-m.fields // acquire
defer func() { m.fields <- fields }() // release
return fields.field1
} |
I added a package for this issue. Please feel free to change it from |
There is also https://github.com/amit-davidson/Chronos |
@timothy-king how did this go? Did you have a chance to get your intern to look into this?
|
Such a tool has been a recurring request, but it's a substantial project as it requires interprocedural analysis to do well. It also needs to degrade gracefully at the boundary between annotated and unannotated portions of the program. I made some initial experiments in this direction many years ago, and one feature I would like to see in the solution is the use of Go itself--not comments--to express the annotations, so that they are subject to type checking, operated on by renaming tools, reported by cross-reference queries, and so on; otherwise they will go as stale and unread as ordinary doc comments. For example, the code below shows a hypothetical annotation.Guards function whose body is empty, but whose presence in the source tells the analysis tool the relationship between the mutex (S.mu) and the fields it guards (S.x, etc). The *S parameter is in effect is a universal ("for all") quantifier.
|
Hey Alan how are you?!?
Personally I have no skin-in-the-game for *how* the annotations work, I
just want them. As to your specific proposal here, this moves the
annotations from where the mutex is declared to somewhere else? I probably
have at least a mild preference for seeing the constraints in the
definition of the data type & specific fields, rather than elsewhere in the
program, but maybe I'm misunderstanding?
…On Tue, Sep 27, 2022 at 9:31 AM Alan Donovan ***@***.***> wrote:
Such a tool has been a recurring request, but it's a substantial project
as it requires interprocedural analysis to do well. It also needs to
degrade gracefully at the boundary between annotated and unannotated
portions of the program.
I made some initial experiments in this direction many years ago, and one
feature I would like to see in the solution is the use of Go itself--not
comments--to express the annotations, so that they are subject to type
checking, operated on by renaming tools, reported by cross-reference
queries, and so on; otherwise they will go as stale and unread as ordinary
doc comments.
For example, the code below shows a hypothetical annotation.Guards
function whose body is empty, but whose presence in the source tells the
analysis tool the relationship between the mutex (S.mu) and the fields it
guards (S.x, etc). The *S parameter in in effect is a universal ("for all")
quantifier.
import "annotation"
type S struct {
mu sync.Mutex
x, y, z int
}
var mu sync.Mutex
var g int
func _(s *S) {
annotation.Guards(mu, g) // a simple relation
annotation.Guards(s.mu, s.x, s.y, s.z) // a relation universally quantified over all S
}
—
Reply to this email directly, view it on GitHub
<#46788 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AQ2F6767HTXABYFZOLFHDHTWALZJZANCNFSM46Z76WQQ>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
We did the internship, and we managed to learn quite a bit. If you are interested in this topic, I strongly encourage you to try out checklocks. We based the internship on modifying that code base. Here are a few of my big take-aways and opinions after doing this:
So some progress happened but big-ish, algorithm questions still remain for me. I am hoping to look into this more at some point. Maybe another internship? |
On Tue, Sep 27, 2022 at 2:17 PM Tim King ***@***.***> wrote:
We did the internship, and we managed to learn quite a bit. If you are
interested in this topic, I strongly encourage you to try out checklocks
<https://github.com/google/gvisor/tree/master/tools/checklocks>. We based
the internship on modifying that code base.
I definitely will! Thanks for letting me know.
Here are a few of my big take-aways and opinions after doing this:
1. the value of lock annotations seems consistent with other languages
the experiments we tried.
2. the lock annotation algorithms for other languages (like LLVM's)
are not yet a perfect match for Go due to defer. The challenge is the
pattern if ... { x.mu.Lock(); defer x.mu.Unlock(); _ = x.guarded ; }
/* code that does not touch mu or guarded */. This pattern is too
common to ignore and should be supported. We worked on getting to a
polynomial time algorithm and had some success with some kinda complex
state representation. But I do not think we yet know a satisfying
polynomial time algorithm for this that will not confuse tool users. Going
out on a limb, I suspect the problems we saw is fixable by recording both
the pre and post lock states of blocks so we can faithfully know when the
result of a meet operations is not an equality, doing 'reversish abstract
interpretation' from the returns to execute the defers, and only reporting
a mismatch when the meet on a reverse post state has a disequal result to
its inputs. I am speculating though. I have not tried this.
Yeah this is a tough one. I'd be tempted to consider this a potential bug
in the program. This is somebody using defer like it was a C++ destructor,
but they're missing a scope:
if ... { func(){ x.mu.Lock(); defer x.mu.Unlock(); _ = x.guarded; }() }
In some ways, this should be a Go-specific warning--"you used defer to
unlock your mutex, but the unlock can happen *much* later than you intend,
maybe wrap in func() { ... }()?". The issue here is that in the original
scenario if ... { x.mu.Lock(); defer x.mu.Unlock(); _ = x.guarded ; } /*
code that does not touch mu or guarded */ there could be some
computationally intensive work in "code that does not touch mu or guarded",
or an RPC, or some other blocking operation that maybe the author did not
intend to be coupled to x.mu.
1. a mutex-hat opt in annotations that mean "the field mu guards the
immediately following fields in the struct" seems largely sufficient after
our experiments. This annotation struck a good balance of feeling minimal
while giving an opt-in signal. It can also be a struct tag.
Yeah this is pretty interesting.
1. function lock annotations still felt a bit too verbose to feel
"Go-like". The challenge we are setting for ourselves is whether we get it
down to *1 annotation* in the vast majority of cases. It would be
great if this could just be "mu guards the following fields". This seems to
require some inter-pocedural inference (but not inter-package). The
algorithm for this inference is not yet settled. I suspect it would also
need to be a bit opinionated: exported methods default to the annotation
'unlocked->unlocked' unless they are named Lock or Unlock() [or need an
annotation otherwise? or unsupported?]. So there would be safe 'guarded by'
patterns it would not support.
So some progress happened but big-ish, algorithm questions still remain
for me. I am hoping to look into this more at some point. Maybe another
internship?
Wow, thank you for sharing your thoughts! It's fascinating to hear this
level of detail.
Take care,
…--George
—
Reply to this email directly, view it on GitHub
<#46788 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AQ2F672JHEXOBGPBMVZZP5DWAM24BANCNFSM46Z76WQQ>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
In issue #24889 there's a short paragraph about static thread safety analysis that clang does for C++ programs:
I'm pretty agnostic as to how some form of static thread safety analysis enters the Go ecosystem, but I would like to have it. I've used this at a previous employer (Google) to great effect, and IMO it would be of great benefit to Go programs as well.
Here's a strawman proposal, more to spur discussion than be a "real" solution. What if a struct is defined with a lock in it like so:
Let's annotate MyStruct to require locking on all of its members:
So if I defined a function that accessed the members and didn't lock, compilation would fail:
But this would work:
And this too:
I know folks don't love the comment pragmas, but I didn't have a better idea. Perhaps the basic gist of tying the lock to a specific struct that there could be some way that's "neater" and "more go like" than the complex clang annotations? With anonymous struct fields making for clean composition?
The text was updated successfully, but these errors were encountered: