projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
899f4a4
)
Fixing a bug in isConflict method.
author
rtrimana
<rtrimana@uci.edu>
Wed, 17 Jun 2020 18:25:42 +0000
(11:25 -0700)
committer
rtrimana
<rtrimana@uci.edu>
Wed, 17 Jun 2020 18:25:42 +0000
(11:25 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index f6903824fc2a9ec388f538b71a44498aefe54420..a483afcc7e6d6f0843b9a168b1c248b0c91ded17 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@
-961,21
+961,21
@@
public class DPORStateReducer extends ListenerAdapter {
private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet) {
ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet) {
ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
- HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();
// Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
// Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
- if (!
exec
RWFieldsMap.containsKey(conflictChoice) ||
+ if (!
conf
RWFieldsMap.containsKey(conflictChoice) ||
executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
return false;
}
// R/W set of choice/event that may have a potential conflict
executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
return false;
}
// R/W set of choice/event that may have a potential conflict
- ReadWriteSet
evtRWSet = exec
RWFieldsMap.get(conflictChoice);
+ ReadWriteSet
confRWSet = conf
RWFieldsMap.get(conflictChoice);
// Check for conflicts with Read and Write fields for Write instructions
Set<String> currWriteSet = currRWSet.getWriteSet();
for(String writeField : currWriteSet) {
int currObjId = currRWSet.writeFieldObjectId(writeField);
// Check for conflicts with Read and Write fields for Write instructions
Set<String> currWriteSet = currRWSet.getWriteSet();
for(String writeField : currWriteSet) {
int currObjId = currRWSet.writeFieldObjectId(writeField);
- if ((
evtRWSet.readFieldExists(writeField) && evt
RWSet.readFieldObjectId(writeField) == currObjId) ||
- (
evtRWSet.writeFieldExists(writeField) && evt
RWSet.writeFieldObjectId(writeField) == currObjId)) {
+ if ((
confRWSet.readFieldExists(writeField) && conf
RWSet.readFieldObjectId(writeField) == currObjId) ||
+ (
confRWSet.writeFieldExists(writeField) && conf
RWSet.writeFieldObjectId(writeField) == currObjId)) {
// Remove this from the write set as we are tracking per memory location
currRWSet.removeWriteField(writeField);
return true;
// Remove this from the write set as we are tracking per memory location
currRWSet.removeWriteField(writeField);
return true;
@@
-985,7
+985,7
@@
public class DPORStateReducer extends ListenerAdapter {
Set<String> currReadSet = currRWSet.getReadSet();
for(String readField : currReadSet) {
int currObjId = currRWSet.readFieldObjectId(readField);
Set<String> currReadSet = currRWSet.getReadSet();
for(String readField : currReadSet) {
int currObjId = currRWSet.readFieldObjectId(readField);
- if (
evtRWSet.writeFieldExists(readField) && evt
RWSet.writeFieldObjectId(readField) == currObjId) {
+ if (
confRWSet.writeFieldExists(readField) && conf
RWSet.writeFieldObjectId(readField) == currObjId) {
// Remove this from the read set as we are tracking per memory location
currRWSet.removeReadField(readField);
return true;
// Remove this from the read set as we are tracking per memory location
currRWSet.removeReadField(readField);
return true;