Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved liveness detection for store exclusives #722

Merged
merged 29 commits into from
Sep 3, 2024
Merged
Changes from 1 commit
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
92d82b1
Split 'addInto' stats into graph and cycle detection counters (#683)
xeren May 27, 2024
016aaf4
UI update (#684)
ThomasHaas May 31, 2024
184fab4
Add support for memcpy_s (#686)
hernanponcedeleon Jun 3, 2024
28885e2
- Added Event.getLocalId/Event.setLocalId() (#688)
ThomasHaas Jun 7, 2024
929b15b
Add support for cttz (count trailing zeros) intrinsic (#689)
hernanponcedeleon Jun 7, 2024
1afd208
Fix addresses in witnesses (#692)
ThomasHaas Jun 12, 2024
6c8baa3
Fix size and offset computations of types (#691)
ThomasHaas Jun 12, 2024
94f90c7
Fix inclusion updates in IBPA (#694)
xeren Jun 13, 2024
8b8389a
Easier handling of nondet choices (#693)
ThomasHaas Jun 13, 2024
2688e01
Fix cttz bug (#696)
hernanponcedeleon Jun 13, 2024
075f03f
Better mem2reg (#697)
ThomasHaas Jun 14, 2024
3291aa0
Model locks as spinloops to avoid wrong liveness bugs (#695)
hernanponcedeleon Jun 17, 2024
489f608
Assertion expressions (#690)
xeren Jun 19, 2024
d917401
Added TagSet, used in AbstractEvent to store tags of events. (#698)
ThomasHaas Jun 19, 2024
fa5a226
Avoid exception in SyntacticContextAnalysis (#699)
hernanponcedeleon Jul 1, 2024
3771432
Add loop bound annotation (#687)
hernanponcedeleon Jul 2, 2024
6356656
Automatically cancel previous CI when new commits are pushed (#700)
hernanponcedeleon Jul 4, 2024
9f44db5
Update JavaSMT version (#701)
hernanponcedeleon Jul 22, 2024
e87cb88
Refactor relation analysis interface (#702)
DIvanov503 Jul 22, 2024
eb15f40
Fix an incorrect term pattern in SyncWith (#706)
DIvanov503 Jul 29, 2024
6582d4a
Extend loop normalization (#705)
hernanponcedeleon Aug 3, 2024
030b16b
Spir-V frontend (#703)
natgavrilenko Aug 12, 2024
cdc0689
Add memory effects to LLVM grammar and better error message (#710)
natgavrilenko Aug 12, 2024
618c3f7
Fix printer OutOfBoundsException (#713)
natgavrilenko Aug 13, 2024
f6d10e2
Compute missing tuples in transitive closure (#718)
DIvanov503 Aug 26, 2024
a81b5fd
Merge branch 'refs/heads/development' into spinloop_excl_store
ThomasHaas Aug 30, 2024
053afd6
Improved DynamicSpinLoopDetection to handle RMWStoreExclusive correctly
ThomasHaas Aug 30, 2024
dc34e7e
Refactored PropertyEncoder.LivenessEncoder and added fairness conditi…
ThomasHaas Aug 30, 2024
b682775
Split Tag.EARLYTERMINATION into EXCEPTITONAL_TERMINATION and NONTERMI…
ThomasHaas Aug 2, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Added TagSet, used in AbstractEvent to store tags of events. (#698)
ThomasHaas authored Jun 19, 2024
commit d9174017867bfce186aa903265f17d19ca1439ce
Original file line number Diff line number Diff line change
@@ -16,7 +16,7 @@
public abstract class AbstractEvent implements Event {

private final MetadataMap metadataMap = new MetadataMap();
private final Set<String> tags;
private final TagSet tags;
private final Set<EventUser> currentUsers = new HashSet<>();
// These ids are dynamically changing during processing.
private transient int globalId = -1; // (Global) ID within a program
@@ -27,12 +27,12 @@ public abstract class AbstractEvent implements Event {
private transient AbstractEvent predecessor;

protected AbstractEvent() {
tags = new HashSet<>();
tags = new TagSet();
}

protected AbstractEvent(AbstractEvent other) {
copyAllMetadataFrom(other);
this.tags = other.tags; // TODO: Dangerous code! A Copy-on-Write Set should be used (e.g. PersistentSet/Map)
this.tags = other.tags.copy();
}

@Override
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
package com.dat3m.dartagnan.program.event;

import java.util.*;

public final class TagSet extends AbstractSet<String> {

private final List<String> sortedTags = new ArrayList<>();

@Override
public boolean add(String tag) {
final int index = Collections.binarySearch(sortedTags, tag);
if (index < 0) {
sortedTags.add(~index, tag);
return true;
}
return false;
}

@Override
public boolean contains(Object o) {
if (o instanceof String tag) {
return Collections.binarySearch(sortedTags, tag) >= 0;
}
return false;
}

@Override
public boolean remove(Object o) {
if (!(o instanceof String tag)) {
return false;
}

final int index = Collections.binarySearch(sortedTags, tag);
if (index >= 0) {
sortedTags.remove(index);
return true;
}
return false;
}

@Override
public Iterator<String> iterator() {
return sortedTags.listIterator();
}

@Override
public int size() {
return sortedTags.size();
}

public TagSet copy() {
final TagSet copy = new TagSet();
copy.sortedTags.addAll(this.sortedTags);
return copy;
}
}