[BUG] Dartagnan errors and hangs sometimes when calling it multiple times simultaniously
Closed this issue · 9 comments
We observed that dartagnan will error or hang sometimes when we start multiple verifications on different files at the same time.
The errors seem to be different every time but all of them seem to stem from the boogie code parsing.
Here are some of the errors we observed.
line 459:52 extraneous input '{' expecting {')', ','}
Exception in thread "main" com.dat3m.dartagnan.exception.ParsingException: Line 459:52 extraneous input '{' expecting {')', ','}
at com.dat3m.dartagnan.exception.ParserErrorListener.syntaxError(ParserErrorListener.java:17)
at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:41)
at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:544)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportUnwantedToken(DefaultErrorStrategy.java:377)
at org.antlr.v4.runtime.DefaultErrorStrategy.sync(DefaultErrorStrategy.java:275)
at com.dat3m.dartagnan.parsers.BoogieParser.func_decl(BoogieParser.java:643)
at com.dat3m.dartagnan.parsers.BoogieParser.main(BoogieParser.java:276)
at com.dat3m.dartagnan.parsers.program.ParserBoogie.parse(ParserBoogie.java:23)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:39)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:32)
at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:105)
line 8861:0 missing '}' at '<EOF>'
Exception in thread "main" com.dat3m.dartagnan.exception.ParsingException: Line 8861:0 missing '}' at '<EOF>'
at com.dat3m.dartagnan.exception.ParserErrorListener.syntaxError(ParserErrorListener.java:17)
at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:41)
at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:544)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:519)
at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
at org.antlr.v4.runtime.Parser.match(Parser.java:206)
at com.dat3m.dartagnan.parsers.BoogieParser.impl_body(BoogieParser.java:1613)
at com.dat3m.dartagnan.parsers.BoogieParser.proc_decl(BoogieParser.java:897)
at com.dat3m.dartagnan.parsers.BoogieParser.main(BoogieParser.java:288)
at com.dat3m.dartagnan.parsers.program.ParserBoogie.parse(ParserBoogie.java:23)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:39)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:32)
at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:105)
line 594:12 mismatched input '<EOF>' expecting {'if', 'int', 'real', 'true', 'false', 'old', '|{', String, Ident, Int, Dec_float, Decimal, Bv_lit, '!', '(', '-', '}'}
Exception in thread "main" com.dat3m.dartagnan.exception.ParsingException: Line 594:12 mismatched input '<EOF>' expecting {'if', 'int', 'real', 'true', 'false', 'old', '|{', String, Ident, Int, Dec_float, Decimal, Bv_lit, '!', '(', '-', '}'}
at com.dat3m.dartagnan.exception.ParserErrorListener.syntaxError(ParserErrorListener.java:17)
at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:41)
at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:544)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportInputMismatch(DefaultErrorStrategy.java:327)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:139)
at com.dat3m.dartagnan.parsers.BoogieParser.attr_or_trigger(BoogieParser.java:7347)
at com.dat3m.dartagnan.parsers.BoogieParser.attr(BoogieParser.java:7221)
at com.dat3m.dartagnan.parsers.BoogieParser.func_decl(BoogieParser.java:602)
at com.dat3m.dartagnan.parsers.BoogieParser.main(BoogieParser.java:276)
at com.dat3m.dartagnan.parsers.program.ParserBoogie.parse(ParserBoogie.java:23)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:39)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:32)
at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:105)
line 10744:18 missing ';' at 'assume'
Exception in thread "main" com.dat3m.dartagnan.exception.ParsingException: Line 10744:18 missing ';' at 'assume'
at com.dat3m.dartagnan.exception.ParserErrorListener.syntaxError(ParserErrorListener.java:17)
at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:41)
at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:544)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:519)
at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
at org.antlr.v4.runtime.Parser.match(Parser.java:206)
at com.dat3m.dartagnan.parsers.BoogieParser.assign_cmd(BoogieParser.java:2543)
at com.dat3m.dartagnan.parsers.BoogieParser.label_or_cmd(BoogieParser.java:2152)
at com.dat3m.dartagnan.parsers.BoogieParser.stmt_list(BoogieParser.java:1691)
at com.dat3m.dartagnan.parsers.BoogieParser.impl_body(BoogieParser.java:1611)
at com.dat3m.dartagnan.parsers.BoogieParser.proc_decl(BoogieParser.java:897)
at com.dat3m.dartagnan.parsers.BoogieParser.main(BoogieParser.java:288)
at com.dat3m.dartagnan.parsers.program.ParserBoogie.parse(ParserBoogie.java:23)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:39)
at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:32)
at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:105)
When we staggered the calls to dartagnan by one second these errors did not occur.
Do the different files also have different names?
I think there may be issues if the file names are identical, because we create intermediate files in the output folder.
There might be name clashes for those files and multiple Dartagnan instance try to write to/read from the same file.
the file names and paths are different for each dartagnan call
I don't understand what you mean by "start multiple verifications on different files at the same time", can you be more precise? Are you calling dartagnan from many consoles "at the same time"? Using some library to start several threads, each making one call?
The error suggests that the boogie file is corrupted, Can you share either your original C file or the bpl one which us generated in the output folder?
I don't understand what you mean by "start multiple verifications on different files at the same time", can you be more precise? Are you calling dartagnan from many consoles "at the same time"? Using some library to start several threads, each making one call?
I am writing a java program that calls dartagnan from multiple threads at the same time.
I was wrong before, the file name is not different, but the path is and it seems like that is the problem.
But I attacked the c files anyways.
main.c
Contains the test and the file that we pass into dartagnan.
#include <pthread.h>
#include <assert.h>
#include "../constants.h"
#include "userCode.h"
#define VALUE_TO_PUSH 42
typedef struct {
STACK *stack;
int *data;
} push_data;
void *producer(void *data) {
push_data *pd = (push_data*) data;
STACK_PUSH(pd->stack, pd->data);
return NULL;
}
void *consumer(void *arg) {
int *val = STACK_POP((STACK*) arg);
assert(val != NULL && *val == VALUE_TO_PUSH);
return NULL;
}
int main(void) {
STACK *test_stack = STACK_NEW();
int initial_element = VALUE_TO_PUSH;
STACK_PUSH(test_stack, &initial_element);
push_data pd[2];
int data[2];
for (int i = 0; i < 2; ++i) {
pd[i].stack = test_stack;
data[i] = VALUE_TO_PUSH;
pd[i].data = &data[i];
}
pthread_t producer_thread1;
pthread_t consumer_thread1;
pthread_t producer_thread2;
pthread_t consumer_thread2;
pthread_create(&producer_thread1, 0, producer, (void *) &pd[0]);
pthread_create(&consumer_thread1, 0, consumer, test_stack);
pthread_join(producer_thread1, NULL);
pthread_join(consumer_thread1, NULL);
pthread_create(&producer_thread2, 0, producer, (void *) &pd[1]);
pthread_create(&consumer_thread2, 0, consumer, test_stack);
pthread_join(producer_thread2, NULL);
pthread_join(consumer_thread2, NULL);
assert(!STACK_EMPTY(test_stack));
return 0;
}userCode.h
Contains the code of the data stucture.
#include <stdatomic.h>
#include <stdlib.h>
#define SUCCESS 0
#define ERR -1
#ifdef FAIL
#define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_RELAXED, __ATOMIC_RELAXED))
#else
#define CAS(ptr, expected, desired) (atomic_compare_exchange_strong_explicit(ptr, expected, desired, __ATOMIC_ACQ_REL, __ATOMIC_RELAXED))
#endif
#ifndef SAFE_STACK
#define SAFE_STACK
typedef struct node {
int *val;
_Atomic(struct node*) next;
} node;
typedef struct {
_Atomic(node*) top;
_Atomic(int) size;
} stack_type;
stack_type *init() {
stack_type *stack = malloc(sizeof(stack_type));
atomic_init(&(stack->top), NULL);
atomic_init(&(stack->size), 0);
return stack;
}
int empty(stack_type *stack) {
if (stack == NULL) {
return 1;
}
node *top = atomic_load_explicit(&stack->top, __ATOMIC_ACQUIRE);
return top == NULL;
}
int size(stack_type *stack) {
if (stack == NULL) {
return 0;
}
return atomic_load_explicit(&stack->size, __ATOMIC_ACQUIRE);
}
int push(stack_type *stack, int *e) {
node *y, *n;
y = malloc(sizeof(node));
if (y == NULL || stack == NULL) {
return ERR;
}
y->val = e;
while(1) {
n = atomic_load_explicit(&stack->top, __ATOMIC_ACQUIRE);
atomic_store_explicit(&y->next, n, __ATOMIC_RELAXED);
if (CAS(&(stack->top), &n, y)) {
int size = atomic_load_explicit(&stack->size, __ATOMIC_ACQUIRE);
atomic_store_explicit(&stack->size, size + 1, __ATOMIC_RELAXED);
break;
}
}
return SUCCESS;
}
int *pop(stack_type *stack) {
node *y, *z;
if (stack == NULL) {
return NULL;
}
while (1) {
y = atomic_load_explicit(&stack->top, __ATOMIC_ACQUIRE);
if (y == NULL) {
return NULL;
} else {
z = atomic_load_explicit(&y->next, __ATOMIC_ACQUIRE);
if (CAS(&(stack->top), &y, z)) {
int size = atomic_load_explicit(&stack->size, __ATOMIC_ACQUIRE);
atomic_store_explicit(&stack->size, size - 1, __ATOMIC_RELAXED);
// retire(y)
break;
}
}
}
return y->val;
}
int *top(stack_type *stack) {
if (stack == NULL) {
return NULL;
}
node *top = atomic_load_explicit(&stack->top, __ATOMIC_ACQUIRE);
if (top == NULL) {
return NULL;
}
return top->val;
}
int destroy(stack_type *stack) {
if (stack == NULL) {
return ERR;
}
while (pop(stack) != NULL) {}
free(stack);
return SUCCESS;
}
#endifconstants.h
Some defines, that shouldn't be relevant to the issue.
#define STACK stack_type
#define STACK_DESTROY destroy
#define STACK_EMPTY empty
#define STACK_SIZE size
#define STACK_NEW init
#define STACK_POP pop
#define STACK_PUSH push
#define STACK_TOP top
#define STACK_SUCCESS SUCCESSIf the file names are not different, then that's surely the problem.
We can see if we can either provide more distinctive names for the intermediate files or if we can provide options to specify the names of the output files.
The problem with using more distinctive names is that we do want the user to be able to easily find the generated files so any cryptic naming scheme that guarantees uniqueness is somewhat counterproductive.
An alternative might be to generate temporary unique files that we use internally, while also creating a persistent copy with proper naming for the user to inspect. The persistent copy might get corrupted due to multi-threaded access, but the internal copies should work fine.
How about building a unique name out of the path to the passed into daratagnan?
You could replace critical characters like / or \ with e.g. underscores. That might produce very long file names, but they would be human-readable and unique.
That certainly works, but filepaths can get extremely long and they tend to have common prefixes for the most part which heavily affects readability.
We will discuss what the best solution is, but for the time being you could do what you propose on your side, that is, give the files unique names before passing them to Dartagnan.
Do we still care about this? I think this problem is rare enough and can be mitigitated on the user's side.
I agree.