Segfault when calling __VERIFIER_method_begin and _end for the linearizability checker

[Daniel-A-W]

I'm having some issues with consistent segfaulting when using the linearizability checker, and it looks like naming methods with __VERIFIER_method_begin and _end is the culprit.

I've built the following small working example containing 3 files: test_client.c which sets up some worker threads, and list.h + list_spec.h which define an ordered list interface and specification. These consistently segfault when I run genmc --collect-lin-spec pointing at test_client.c. Disabling state space estimation doesn't fix it, and neither does changing memory model. Removing the __VERIFIER_method_ functions does fix it, and it happily generates a spec file. Running genmc without the linearizability checker also works fine and produces no errors (except some expected complaints about unfreed memory).

This could be user error, I'm not sure if I'm supposed to register these methods with the checker somehow, but I get the same segfault issue when trying to use the mpc template instead of rolling my own client file.

test_client.c:

#include <pthread.h>
#include <stdio.h>
#include <genmc.h>
#include "list_spec.h"
static List l;

#ifndef THREADS
#define THREADS 3  
#endif

/* =========================================================================
 * Worker thread
 * inserts its own thread id into list
 * ========================================================================= */
static void *inserter() {
    uint64_t val = pthread_self();
    __VERIFIER_method_begin("list_insert", val);
    int ok = list_insert(&l, val);
    __VERIFIER_method_end("list_insert", ok);
    assert(ok == 1);
    return NULL;
}


int main(void) {
    __VERIFIER_thread_t threads[THREADS];
    threads[0] = __VERIFIER_spawn(inserter, NULL);
    for (int i = 1; i < THREADS; ++i)
      threads[i] = __VERIFIER_spawn_symmetric(inserter, NULL, threads[i-1]);

    for (int i = 0; i < THREADS; ++i)
        __VERIFIER_join(threads[i]);

    return 0;
}

Header file for the List interface:

#pragma once
#include <stdlib.h>
// List with int64 nodes held in ascending order
typedef struct List {
    uint64_t      head;
    struct List          *tail;
} List;

static List* cat(List* tl, uint64_t val) {
  List* l = malloc(sizeof(struct List));
  l->head = val;
  l->tail = tl;
  return l;
}

static int list_insert(List *l, uint64_t val);
static int list_remove(List *l, uint64_t val);

And list_spec.h :

#include <genmc.h>
#include "list.h"
__VERIFIER_plock_t plock;

static int list_insert(List *l, uint64_t val) {
  __VERIFIER_plock_lock(&plock);
  if (l == NULL) {
    l = cat(NULL, val);
    __VERIFIER_plock_unlock(&plock);
    return 1;
  }
  List* prev = l;
  l = l->tail;
  while (l != NULL && l->head < val) {
    prev = l;
    l = l->tail;
  }
  List* new_node = cat(l, val);
  prev->tail = new_node;
  __VERIFIER_plock_unlock(&plock);
  return 1;
}
static int list_remove(List *l, uint64_t val) {
  if (l == NULL) return 0;
  __VERIFIER_plock_lock(&plock);
  List* prev = l;
  l = l->tail;
  while (l != NULL && l->head < val) {
    prev = l;
    l = l->tail;
  }
  // now either l == NULL (end of list) or l->head > val (not in list) or l->head == val (found value)
  if (l == NULL || l->head != val) {
    __VERIFIER_plock_unlock(&plock);
    return 0;
  }
  prev->tail = l->tail;
  free(l);
  __VERIFIER_plock_unlock(&plock);
  return 1;
}