Locksmith - Tutorial

A simple race: `simple-race.c`

The following program is similar to simple.c, with one major difference. Now main also accesses shared at line 14, but without holding lock:

 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   shared = 1;
15   return 1;
16 }
17
18 void *run(void *arg) {
19   pthread_mutex_lock(&lock);
20   shared++;
21   pthread_mutex_unlock(&lock);
22   return NULL;
23 }

Running Locksmith on that program gives the output:

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

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

shared: &shared:simple-race.c:4

Warning: Possible data race: &shared:simple-race.c:4 is not protected!
 references:
  dereference of &shared:simple-race.c:4 at simple-race.c:20
    &shared:simple-race.c:4
  locks acquired:
    concrete lock:simple-race.c:11
    lock:simple-race.c:3
  in: FORK at simple-race.c:13


  dereference of &shared:simple-race.c:4 at simple-race.c:20
    &shared:simple-race.c:4
  locks acquired:
    concrete lock:simple-race.c:11
    lock:simple-race.c:3
  in: FORK at simple-race.c:12


  dereference of &shared:simple-race.c:4 at simple-race.c:14
    &shared:simple-race.c:4
  locks acquired:
    <empty>
  in: main at simple-race.c:8


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

LockSmith run for: 0.060000 seconds

First, Locksmith prints a list of all shared memory locations, since it was called using the flag --list-shared. As in the case of simple.c, it lists only &shared. To make the output easier to follow for complex programs that span many files, each lock and location is printed along with the point in the program source where it is defined or allocated. So, Locksmith refers to the location of the global variable shared which is defined at line 4 as &shared:simple-race.c:4.

Next, Locksmith prints a warning, consisting of a title:

  Warning: Possible data race: &shared:simple-race.c:4 is not protected!

that states the location where a possible race is detected, along with the problem. In this case, the location is &shared:simple-race.c:4 and it has an empty protection set. After the warning title, Locksmith prints a list of references. This corresponds to all places in the program where that location might be accessed. The first access listed is:

  dereference of &shared:simple-race.c:4 at simple-race.c:20
    &shared:simple-race.c:4
  locks acquired:
    concrete lock:simple-race.c:11
    lock:simple-race.c:3
  in: FORK at simple-race.c:13

The first line lists the location where the access happens. In this case it is in line 20. Then, Locksmith prints the path from the allocation of the memory location to the actual pointer accessed at that dereference. In this example, the allocated pointer is itself dereferenced, so there is no path printed.

Following that, Locksmith prints a list of all the acquired locks at that point. In this case, it is only the lock variable lock, defined at line 3. However, simply defining a variable of lock type does not create a lock; we need to initialize the lock before using it. So, we treat the variable lock defined at line 3 as a lock variable, and the lock initialization that happens in line 11 as a concrete lock. Since lock:shared-race.c:11 aliases (or contains) the lock created at line 11, we list both locks in the acquired set.

The final line in the description of this access is the path of the access. In this case, the path listed is:

  in: FORK at simple-race.c:13

This means that this dereference occurs in the thread starting at the fork at line 13. This thread starts by calling the function run, in which this dereference occurs, so the path is simple in this case. Locksmith treats functions context sensitively, meaning that it differentiates between two calls of the same function. So, the dereference paths list the lines where a function is invoked.

A simple race: simple-race.c

A simple race: `simple-race.c`