Locksmith - Main

Overview

Locksmith is a static analysis tool that tries to find data races in multithreaded C programs. To do that, it implements a static version of the Lockset algorithm. A race occurs whenever two threads access a memory location without any synchronization, and one of the accesses is a write. Locksmith analyzes multithreaded programs that use locks (or mutexes) to protect accesses to shared locations, and tries to discover which, if any, locks protect each shared location. Whenever an access to a shared memory location is not protected by any lock, it potentially is a race.

Usage

Locksmith by default works for applications written in C, that use POSIX threads for parallelism, and treats pthread_mutex_t as a special lock type. It can also be configured to work with the spin locks found in the Linux kernel, or any other locking primitives, by loading a different configuration file. Locksmith is released for download under the BSD license. See the corresponding download page for installation instructions.

For example, consider the following program, simple.c:

 1 #include <pthread.h>
 2
 3 pthread_mutex_t lock;
 4 int shared;
 5
 6 void* run(void*);
 7
 8 int main() {
 9   pthread_t t1, t2;
10
11   pthread_mutex_init(&lock, NULL);
12   pthread_create(&t1, NULL, run, NULL);
13   pthread_create(&t2, NULL, run, NULL);
14   return 1;
15 }
16
17 void *run(void *arg) {
18   pthread_mutex_lock(&lock);
19   shared++;
20   pthread_mutex_unlock(&lock);
21   return NULL;
22 }

If we run Locksmith on simple.c the output will be:

$ cilly --list-shared --list-guardedby simple.c

************************* STARTING *************************

shared: &shared:simple.c:4
&shared:simple.c:4 is protected by:
  concrete lock:simple.c:11
  lock:simple.c:3

*************************** DONE ***************************

LockSmith run for: 0.010000 seconds

This means that the address of the global variable shared is found to be shared between two threads. Indeed, both threads run the run function, which accesses shared. Furthermore, all accesses to &shared are protected by the lock created at line 11 of simple.c, by the call to pthread_mutex_init. We consider all locks that are created by an explicit call to pthread_mutex_init (or the static initilizer for globals) to be concrete. Finally, the second entry in the protection set corresponds to an alias of the above concrete lock, stored at the variable lock, which is declared at line 3. For more examples of running Locksmith and more detailed explanation of the output, please refer to the tutorial.

People

Funding

This material is based upon work supported by the National Science Foundation under Grant No. CCF-0541036, Scalable, Precise, and Effective Analyses for Detecting Race Conditions. Any opinions, findings and conclusions or recome ndations expressed in this material are those of the author(s) and do not necess arily reflect the views of the National Science Foundation (NSF).