Skip to content

Commit

Permalink
Thread cf & must edges (#494)
Browse files Browse the repository at this point in the history 
Add proper control-flow dependencies between spawned threads and their spawners/creators
  • Loading branch information
@ThomasHaas
ThomasHaas authored Aug 3, 2023
1 parent 7b07232 commit 16d4e0e
Show file tree
Hide file tree
Showing 17 changed files with 400 additions and 412 deletions.
40 changes: 25 additions & 15 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
import com.dat3m.dartagnan.program.event.core.CondJump;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.Label;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
import com.dat3m.dartagnan.program.event.core.utils.RegWriter;
import com.dat3m.dartagnan.program.memory.Memory;
import com.google.common.base.Preconditions;
Expand All @@ -21,7 +22,9 @@
import org.sosy_lab.java_smt.api.*;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;

import java.util.*;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;

import static com.dat3m.dartagnan.GlobalSettings.getArchPrecision;
import static com.dat3m.dartagnan.configuration.OptionNames.INITIALIZE_REGISTERS;
Expand Down Expand Up @@ -109,23 +112,30 @@ public BooleanFormula encodeControlFlow() {

private BooleanFormula encodeThreadCF(Thread thread) {
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();

Map<Label, Set<CondJump>> labelJumpMap = new HashMap<>();
Event pred = null;
final ThreadStart startEvent = thread.getEntry();
final List<BooleanFormula> enc = new ArrayList<>();
for(Event e : thread.getEntry().getSuccessors()) {

final BooleanFormula cfStart = context.controlFlow(startEvent);
if (startEvent.getCreator() == null) {
enc.add(cfStart);
} else if (startEvent.mayFailSpuriously()) {
enc.add(bmgr.implication(cfStart, context.execution(startEvent.getCreator())));
} else {
enc.add(bmgr.equivalence(cfStart, context.execution(startEvent.getCreator())));
}
enc.add(startEvent.encodeExec(context));

Event pred = startEvent;
for(Event e : startEvent.getSuccessor().getSuccessors()) {
// Immediate control flow
BooleanFormula cfCond = pred == null ? bmgr.makeTrue() : context.controlFlow(pred);
BooleanFormula cfCond = context.controlFlow(pred);
if (pred instanceof CondJump jump) {
cfCond = bmgr.and(cfCond, bmgr.not(context.jumpCondition(jump)));
// NOTE: we need to register the actual jumps here, because the
// listener sets of labels is too large (it contains old copies)
labelJumpMap.computeIfAbsent(jump.getLabel(), key -> new HashSet<>()).add(jump);
}

// Control flow via jumps
if (e instanceof Label) {
for (CondJump jump : labelJumpMap.getOrDefault(e, Collections.emptySet())) {
if (e instanceof Label label) {
for (CondJump jump : label.getJumpSet()) {
cfCond = bmgr.or(cfCond, bmgr.and(context.controlFlow(jump), context.jumpCondition(jump)));
}
}
Expand All @@ -145,7 +155,7 @@ public BooleanFormula encodeMemory() {
// For all objects, their 'final' value fetched here represents their constant value.
BooleanFormula[] addrExprs;
if(getArchPrecision() > -1) {
final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
addrExprs = memory.getObjects().stream()
.map(addr -> bvmgr.equal((BitvectorFormula) context.encodeFinalExpression(addr),
bvmgr.makeBitvector(getArchPrecision(), addr.getValue().intValue())))
Expand All @@ -154,7 +164,7 @@ public BooleanFormula encodeMemory() {
final IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
addrExprs = memory.getObjects().stream()
.map(addr -> imgr.equal((IntegerFormula) context.encodeFinalExpression(addr),
imgr.makeNumber(addr.getValue().intValue())))
imgr.makeNumber(addr.getValue().intValue())))
.toArray(BooleanFormula[]::new);
}
return fmgr.getBooleanFormulaManager().and(addrExprs);
Expand Down Expand Up @@ -209,9 +219,9 @@ public BooleanFormula encodeDependencies() {
}

public BooleanFormula encodeFilter() {
return context.getTask().getProgram().getFilterSpecification() != null ?
return context.getTask().getProgram().getFilterSpecification() != null ?
context.getTask().getProgram().getFilterSpecification().encode(context) :
context.getBooleanFormulaManager().makeTrue();
context.getBooleanFormulaManager().makeTrue();
}

public BooleanFormula encodeFinalRegisterValues() {
Expand Down
12 changes: 6 additions & 6 deletions dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
import com.dat3m.dartagnan.program.event.core.CondJump;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.Label;
import com.dat3m.dartagnan.program.event.core.Skip;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
import com.dat3m.dartagnan.program.event.metadata.OriginalId;
import com.dat3m.dartagnan.program.memory.Memory;
import com.dat3m.dartagnan.program.memory.MemoryObject;
Expand Down Expand Up @@ -104,14 +104,13 @@ public void setAssertFilter(AbstractAssert ass) {
// ----------------------------------------------------------------------------------------------------------------
// Threads and Functions

// This method creates a "default" thread that has no parameters, no return value, and runs unconditionally.
// It is only useful for creating threads of Litmus code.
public Thread newThread(String name, int tid) {
if(id2FunctionsMap.containsKey(tid)) {
throw new MalformedProgramException("Function or thread with id " + tid + " already exists.");
}
// TODO: We use a default thread type with no parameters and no return type for now
// because the function type is still ignored for threads. In the future, we will assign
// proper types.
final Thread thread = new Thread(name, DEFAULT_THREAD_TYPE, List.of(), tid, EventFactory.newSkip());
final Thread thread = new Thread(name, DEFAULT_THREAD_TYPE, List.of(), tid, EventFactory.newThreadStart(null));
id2FunctionsMap.put(tid, thread);
program.addThread(thread);
return thread;
Expand Down Expand Up @@ -291,7 +290,8 @@ public void newScopedThread(String name, int id, int ctaID, int gpuID) {
if(id2FunctionsMap.containsKey(id)) {
throw new MalformedProgramException("Function or thread with id " + id + " already exists.");
}
Skip threadEntry = EventFactory.newSkip();
// Litmus threads run unconditionally (have no creator) and have no parameters/return types.
ThreadStart threadEntry = EventFactory.newThreadStart(null);
PTXThread ptxThread = new PTXThread(name, DEFAULT_THREAD_TYPE, List.of(), id, threadEntry, gpuID, ctaID);
id2FunctionsMap.put(id, ptxThread);
program.addThread(ptxThread);
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/ScopedThread/PTXThread.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@

import com.dat3m.dartagnan.expression.type.FunctionType;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;

import java.util.List;

public class PTXThread extends ScopedThread {

// There is a unique system level

public PTXThread(String name, FunctionType funcType, List<String> parameterNames, int id, Event entry,
public PTXThread(String name, FunctionType funcType, List<String> parameterNames, int id, ThreadStart entry,
int GpuId, int CtaId) {
super(name, funcType, parameterNames, id, entry);
this.scopeIds.put(Tag.PTX.SYS, 0);
Expand Down
4 changes: 2 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/ScopedThread/ScopedThread.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

import com.dat3m.dartagnan.expression.type.FunctionType;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;

import java.util.ArrayList;
import java.util.LinkedHashMap;
Expand All @@ -17,7 +17,7 @@ public class ScopedThread extends Thread {
// is important, thus we use a LinkedHashMap
protected final Map<String, Integer> scopeIds = new LinkedHashMap<>();

public ScopedThread(String name, FunctionType funcType, List<String> parameterNames, int id, Event entry) {
public ScopedThread(String name, FunctionType funcType, List<String> parameterNames, int id, ThreadStart entry) {
super(name, funcType, parameterNames, id, entry);
}

Expand Down
9 changes: 7 additions & 2 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,24 @@
package com.dat3m.dartagnan.program;

import com.dat3m.dartagnan.expression.type.FunctionType;
import com.dat3m.dartagnan.program.event.core.Event;
import com.dat3m.dartagnan.program.event.core.threading.ThreadStart;
import com.google.common.base.Preconditions;

import java.util.List;

public class Thread extends Function {

public Thread(String name, FunctionType funcType, List<String> parameterNames, int id, Event entry) {
public Thread(String name, FunctionType funcType, List<String> parameterNames, int id, ThreadStart entry) {
super(name, funcType, parameterNames, id, entry);
Preconditions.checkArgument(id >= 0, "Invalid thread ID");
Preconditions.checkNotNull(entry, "Thread entry event must be not null");
}

@Override
public ThreadStart getEntry() {
return (ThreadStart) entry;
}

@Override
public String toString() {
return String.format("T%d:%s", id, name);
Expand Down
Loading

0 comments on commit 16d4e0e

Please sign in to comment.