Skip to content

Commit

Permalink
Add ThreadModel and remove useless data structures
Browse files Browse the repository at this point in the history 
Signed-off-by: Tianrui Zheng <tianrui.zheng@huawei.com>
  • Loading branch information
Tianrui Zheng committed Nov 26, 2024
1 parent 89107bd commit 8e8a4ae
Show file tree
Hide file tree
Showing 7 changed files with 91 additions and 185 deletions.
1 change: 0 additions & 1 deletion dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.Model;
import org.sosy_lab.common.configuration.InvalidConfigurationException;

import java.math.BigInteger;
import java.util.List;
Expand Down
120 changes: 18 additions & 102 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelNext.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,28 +2,25 @@

import com.dat3m.dartagnan.program.event.Event;
import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.filter.Filter;
import com.dat3m.dartagnan.program.memory.MemoryObject;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.program.Program;
import com.dat3m.dartagnan.verification.model.event.*;
import com.dat3m.dartagnan.verification.model.relation.RelationModel;
import com.dat3m.dartagnan.wmm.Relation;

import java.math.BigInteger;
import java.util.*;

import static com.google.common.base.Preconditions.checkNotNull;


// This is a new implementation of ExecutionModel which serves as the data structure
// representing an execution in Dartagnan. It contains instances of EventModel for events
// and RelationModel for relations. It is used only by ExecutionGraphVisualizer so far.
public class ExecutionModelNext {
private final ExecutionModelManager manager;

private final List<Thread> threadList;
private final List<ThreadModel> threadList;
private final List<EventModel> eventList;
private final Map<Thread, List<EventModel>> threadEventsMap;
private final Map<Event, EventModel> eventMap;
private final Map<Relation, RelationModel> relationMap;
private final Map<String, RelationModel> relationNameMap;
Expand All @@ -32,39 +29,13 @@ public class ExecutionModelNext {
private final Map<BigInteger, Set<LoadModel>> addressReadsMap;
private final Map<BigInteger, Set<StoreModel>> addressWritesMap;
private final Map<BigInteger, Set<MemoryEventModel>> addressAccessesMap;
private final Map<BigInteger, StoreModel> addressInitMap;
private final Map<String, Set<FenceModel>> fenceMap;
private final Map<Thread, List<List<EventModel>>> atomicBlocksMap;

private final Map<LoadModel, StoreModel> readWriteMap;
private final Map<StoreModel, Set<LoadModel>> writeReadsMap;

private final Map<BigInteger, List<StoreModel>> coherenceMap;

// Views
private List<Thread> threadListView;
private List<EventModel> eventListView;
private Map<Thread, List<EventModel>> threadEventsMapView;
private Map<Event, EventModel> eventMapView;
private Map<Relation, RelationModel> relationMapView;
private Map<String, RelationModel> relationNameMapView;
private Map<MemoryObject, MemoryObjectModel> memoryLayoutMapView;
private Map<BigInteger, Set<LoadModel>> addressReadsMapView;
private Map<BigInteger, Set<StoreModel>> addressWritesMapView;
private Map<BigInteger, Set<MemoryEventModel>> addressAccessesMapView;
private Map<BigInteger, StoreModel> addressInitMapView;
private Map<String, Set<FenceModel>> fenceMapView;
private Map<Thread, List<List<EventModel>>> atomicBlocksMapView;
private Map<LoadModel, StoreModel> readWriteMapView;
private Map<StoreModel, Set<LoadModel>> writeReadsMapView;
private Map<BigInteger, List<StoreModel>> coherenceMapView;

ExecutionModelNext(ExecutionModelManager manager) {
this.manager = manager;

threadList = new ArrayList<>();
eventList = new ArrayList<>();
threadEventsMap = new HashMap<>();
eventMap = new HashMap<>();
relationMap = new HashMap<>();
relationNameMap = new HashMap<>();
Expand All @@ -73,40 +44,11 @@ public class ExecutionModelNext {
addressReadsMap = new HashMap<>();
addressWritesMap = new HashMap<>();
addressAccessesMap = new HashMap<>();
addressInitMap = new HashMap<>();
fenceMap = new HashMap<>();
atomicBlocksMap = new HashMap<>();

readWriteMap = new HashMap<>();
writeReadsMap = new HashMap<>();

coherenceMap = new HashMap<>();

createViews();
}

private void createViews() {
threadListView = Collections.unmodifiableList(threadList);
eventListView = Collections.unmodifiableList(eventList);
threadEventsMapView = Collections.unmodifiableMap(threadEventsMap);
eventMapView = Collections.unmodifiableMap(eventMap);
relationMapView = Collections.unmodifiableMap(relationMap);
relationNameMapView = Collections.unmodifiableMap(relationNameMap);
memoryLayoutMapView = Collections.unmodifiableMap(memoryLayoutMap);
addressReadsMapView = Collections.unmodifiableMap(addressReadsMap);
addressWritesMapView = Collections.unmodifiableMap(addressWritesMap);
addressAccessesMapView = Collections.unmodifiableMap(addressAccessesMap);
addressInitMapView = Collections.unmodifiableMap(addressInitMap);
fenceMapView = Collections.unmodifiableMap(fenceMap);
atomicBlocksMapView = Collections.unmodifiableMap(atomicBlocksMap);
readWriteMapView = Collections.unmodifiableMap(readWriteMap);
writeReadsMapView = Collections.unmodifiableMap(writeReadsMap);
coherenceMapView = Collections.unmodifiableMap(coherenceMap);
}

public void addThreadEvents(Thread thread, List<EventModel> events) {
threadList.add(thread);
threadEventsMap.put(thread, events);
threadList.add(new ThreadModel(thread, events));
}

public void addEvent(Event e, EventModel eModel) {
Expand Down Expand Up @@ -148,40 +90,28 @@ public void addAddressWrite(BigInteger address, StoreModel write) {
addressAccessesMap.get(address).add((MemoryEventModel) write);
}

public void addAddressInit(BigInteger address, StoreModel init) {
addressInitMap.put(address, init);
}

public void addFence(FenceModel fence) {
fenceMap.computeIfAbsent(fence.getName(), key -> new HashSet<>()).add(fence);
}

public void addAtomicBlocks(Thread thread, List<List<EventModel>> atomics) {
atomicBlocksMap.put(thread, atomics);
}

public void addReadWrite(LoadModel read, StoreModel write) {
readWriteMap.put(read, write);
}

public void addWriteRead(StoreModel write, LoadModel read) {
writeReadsMap.computeIfAbsent(write, key -> new HashSet<>()).add(read);
public ExecutionModelManager getManager() {
return manager;
}

public void addCoherenceWrites(BigInteger address, List<StoreModel> writes) {
coherenceMap.put(address, writes);
public List<ThreadModel> getThreadList() {
return Collections.unmodifiableList(threadList);
}

public ExecutionModelManager getManager() {
return manager;
public List<EventModel> getEventList() {
return Collections.unmodifiableList(eventList);
}

public List<Thread> getThreads() {
return threadList;
public List<EventModel> getVisibleEventList() {
return eventList.stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList();
}

public List<EventModel> getEventList() {
return eventListView;
public List<EventModel> getEventsByFilter(Filter filter) {
return eventList.stream().filter(e -> filter.apply(e.getEvent())).toList();
}

public EventModel getEventModelById(int id) {
Expand All @@ -192,41 +122,27 @@ public EventModel getEventModelByEvent(Event event) {
return eventMap.get(event);
}

public List<EventModel> getEventModelsToShow(Thread t) {
return threadEventsMap.get(t).stream()
.filter(e -> e.hasTag(Tag.VISIBLE) || e.isLocal() || e.isAssert())
.toList();
}

public RelationModel getRelationModel(String name) {
return relationNameMap.get(name);
}

public Map<Thread, List<EventModel>> getThreadEventsMap() {
return threadEventsMapView;
}

public Map<MemoryObject, MemoryObjectModel> getMemoryLayoutMap() {
return memoryLayoutMapView;
return Collections.unmodifiableMap(memoryLayoutMap);
}

public Map<BigInteger, Set<LoadModel>> getAddressReadsMap() {
return addressReadsMapView;
return Collections.unmodifiableMap(addressReadsMap);
}

public Map<BigInteger, Set<StoreModel>> getAddressWritesMap() {
return addressWritesMapView;
return Collections.unmodifiableMap(addressWritesMap);
}

public Map<BigInteger, Set<MemoryEventModel>> getAddressAccessesMap() {
return addressAccessesMapView;
}

public Map<BigInteger, StoreModel> getAddressInitMap() {
return addressInitMapView;
return Collections.unmodifiableMap(addressAccessesMap);
}

public Map<Thread, List<List<EventModel>>> getAtomicBlocksMap() {
return atomicBlocksMapView;
return Collections.unmodifiableMap(atomicBlocksMap);
}
}
37 changes: 37 additions & 0 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ThreadModel.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
package com.dat3m.dartagnan.verification.model;

import com.dat3m.dartagnan.program.event.Tag;
import com.dat3m.dartagnan.program.Thread;
import com.dat3m.dartagnan.verification.model.event.EventModel;

import java.util.Collections;
import java.util.List;


public class ThreadModel {
private final Thread thread;
private final List<EventModel> eventList;

public ThreadModel(Thread thread, List<EventModel> eventList) {
this.thread = thread;
this.eventList = eventList;
}

public int getId() {
return thread.getId();
}

public List<EventModel> getEventList() {
return Collections.unmodifiableList(eventList);
}

public List<EventModel> getVisibleEventList() {
return eventList.stream().filter(e -> e.hasTag(Tag.VISIBLE)).toList();
}

public List<EventModel> getEventModelsToShow() {
return eventList.stream()
.filter(e -> e.hasTag(Tag.VISIBLE) || e.isLocal() || e.isAssert())
.toList();
}
}
6 changes: 1 addition & 5 deletions dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/event/EventModelManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ private void extractEvents() {
}

if (eventList.size() > 0) {
executionModel.addThreadEvents(t, Collections.unmodifiableList(eventList));
executionModel.addThreadEvents(t, eventList);

List<List<EventModel>> atomicBlocks = new ArrayList<>(atomicBlockRanges.size());
for (int i = 0; i < atomicBlockRanges.size(); i++) {
Expand Down Expand Up @@ -138,9 +138,6 @@ private EventModel createAndInitializeModel(Event e) {
} else if (e.hasTag(Tag.WRITE)) {
em = new StoreModel(e);
executionModel.addAddressWrite(address, (StoreModel) em);
if (em.isInit()) {
executionModel.addAddressInit(address, (StoreModel) em);
}
} else {
em = new MemoryEventModel(e);
}
Expand All @@ -164,7 +161,6 @@ private EventModel createAndInitializeModel(Event e) {
} else if (e.hasTag(Tag.FENCE)) {
String name = ((GenericVisibleEvent) e).getName();
em = new FenceModel(e, name);
executionModel.addFence((FenceModel) em);
} else if (e instanceof Assert) {
em = new AssertModel((Assert) e);
} else if (e instanceof Local) {
Expand Down
Loading

0 comments on commit 8e8a4ae

Please sign in to comment.