Skip to content
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

Mutex/thread sanity analysis #176

Open
sim642 opened this issue Apr 6, 2021 · 3 comments
Open

Mutex/thread sanity analysis #176

sim642 opened this issue Apr 6, 2021 · 3 comments
Labels

Comments

@sim642
Copy link
Member

sim642 commented Apr 6, 2021

While debugging some benchmark programs, I noticed they themselves contain silly bugs:

  1. Forgetting to unlock a mutex (e.g. at early return), which makes any following call of the function deadlock or undefined behavior: https://github.com/goblint/bench/blob/16ee6e2dfa54881be2161cb5bb6eee8cce5736d7/pthread/pfscan_comb.c#L1234-L1237.
  2. Unlocking a mutex, which isn't held, which is undefined behavior, e.g. forgetting to relock at the end of a loop for protected condition check: https://github.com/goblint/bench/blob/16ee6e2dfa54881be2161cb5bb6eee8cce5736d7/pthread/smtprc_comb.c#L2379-L2386. MayLock Analysis & Sanity Checks of Mutex Usage & Analysis of Mutex Types #839
  3. Re-initializing a locked mutex.

At least in the case of non-recursive mutexes, these issues and other similar ones might be useful to have some simple analysis for to warn about.

@sim642 sim642 added the feature label Apr 6, 2021
@sim642
Copy link
Member Author

sim642 commented Jun 22, 2021

A related point that arose during GobCon is that joining a thread multiple times is also undefined behavior.

@sim642 sim642 changed the title Mutex sanity analysis Mutex/thread sanity analysis Jun 22, 2021
@michael-schwarz
Copy link
Member

michael-schwarz commented Jul 28, 2022

Other instances Helmut and I identified as easy wins to claim we are fully-fledged analyzer of concurrency bugs:

@michael-schwarz
Copy link
Member

Related #1100

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants