Skip to content

Commit

Permalink
Dev/ashish (#753)
Browse files Browse the repository at this point in the history 
* [PEx] Change schedule choice from PMachine to PMachineId

* [PEx] Major revamping of Choice: 1/n

Old schedule/data choice changed to schedule/data SearchUnit

Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?>

TODO: clean up Schedule with new class structure

* Revert "[PEx] Major revamping of Choice: 1/n"

This reverts commit 53c5d15.

* [PEx] Separates unexplored choices from schedule

* [PEx] Cleanup and minor corrections to recent changes to SearchTask

* [PEx] Minor correction

* [PEx] Corrections to new backtracking logic

* Ongoing Changes

* Week 6 tasks

* discussed changes

* discussed changes

* Recent Changes

* [PEx] Add thread-safe code for search strategies, minor cleanup

* [PEx] Refactoring and cleanup

* More changes

* New changes

* Changes

* Changes

* Remove optional parameters in Monitor (#747)

* Changes

* Changes

* Changes

* Local CHanges

* All changes

* Changes

* Required changes

* 1. Changes made. 2. For hardcoded log path, need to know where scripts are placed are inside the P folder (else can then change) 3. For nproc 4, added code for killing other threads when bugfoundException is raised

* Hardcoded path changed

* Added code for gracefully interrupting other threads, but confusing error: comment and uncomment L151 and L152, and run for both

* nproc: 4, bugs < 86

* Changes

---------

Co-authored-by: Aman Goel <[email protected]>
Co-authored-by: mchadalavada <[email protected]>
  • Loading branch information
@xashisk @aman-goel @mchadalavada
3 people authored Aug 5, 2024
1 parent 7644120 commit 419f335
Show file tree
Hide file tree
Showing 20 changed files with 423 additions and 195 deletions.
2 changes: 2 additions & 0 deletions Src/PRuntimes/PExplicitRuntime/regressionTestScript 11.14.59 AM.sh
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
./scripts/build.sh
mvn test
176 changes: 125 additions & 51 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@

import java.time.Duration;
import java.time.Instant;
import java.util.ArrayList;
import java.util.concurrent.*;
import java.util.*;

/**
* Represents the runtime executor that executes the analysis engine
Expand All @@ -25,27 +25,25 @@ public class RuntimeExecutor {
private static ThreadPoolExecutor executor;
private static ArrayList<Future<Integer>> futures = new ArrayList<>();
private static ArrayList<ExplicitSearchScheduler> schedulers = new ArrayList<>();
private static List<Thread> threads = new ArrayList<>();

private static void runWithTimeout(long timeLimit)
throws TimeoutException,
InterruptedException,
RuntimeException {
try { // PIN: If thread gets exception, need to kill the other threads.
try {
if (timeLimit > 0) {

for (Future<Integer> future : futures) {
// Future<Integer> future = futures.get(i);
future.get(timeLimit, TimeUnit.SECONDS);
}

} else {

for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
Future<Integer> future = futures.get(i);
for (Future<Integer> future : futures) {
future.get();
}
}
} catch (TimeoutException | BugFoundException e) {
} catch (TimeoutException e) {
throw e;
} catch (BugFoundException e) { // Dont merge with TimeoutException catch block, easier for seeing race conditions
throw e;
} catch (OutOfMemoryError e) {
throw new MemoutException(e.getMessage(), MemoryMonitor.getMemSpent(), e);
Expand Down Expand Up @@ -84,9 +82,16 @@ private static void preprocess() {
PExplicitLogger.logInfo(String.format("... Checker is using '%s' strategy (seed:%s)",
PExplicitGlobal.getConfig().getSearchStrategyMode(), PExplicitGlobal.getConfig().getRandomSeed()));

executor = (ThreadPoolExecutor) Executors.newFixedThreadPool(PExplicitGlobal.getMaxThreads());
ThreadFactory threadFactory = new ThreadFactory() {
@Override
public Thread newThread(Runnable r) {
Thread thread = new Thread(r);
threads.add(thread);
return thread;
}
};

// PExplicitGlobal.setResult("error"); // TODO: Set Results, need to take care of.
executor = (ThreadPoolExecutor) Executors.newFixedThreadPool(PExplicitGlobal.getMaxThreads(), threadFactory);

double preSearchTime =
TimeMonitor.findInterval(TimeMonitor.getStart());
Expand All @@ -98,15 +103,18 @@ private static void preprocess() {
}

private static void process(boolean resume) throws Exception {

ArrayList<TimedCall> timedCalls = new ArrayList<>();
try {
// create and add first task through scheduler 0
schedulers.get(0).getSearchStrategy().createFirstTask();

ArrayList<TimedCall> timedCalls = new ArrayList<>();

for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
timedCalls.add(new TimedCall(schedulers.get(i), resume, i));
}


for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
Future<Integer> future = executor.submit(timedCalls.get(i));
futures.add(future);
Expand All @@ -122,75 +130,141 @@ private static void process(boolean resume) throws Exception {

runWithTimeout((long) PExplicitGlobal.getConfig().getTimeLimit());

} catch (TimeoutException e) {
PExplicitGlobal.setStatus(STATUS.TIMEOUT);
throw new Exception("TIMEOUT", e);
} catch (MemoutException | OutOfMemoryError e) {
PExplicitGlobal.setStatus(STATUS.MEMOUT);
throw new Exception("MEMOUT", e);
} catch (BugFoundException e) {
PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
}
catch (MemoutException | OutOfMemoryError e) {
for (Thread thread : threads) {
if (thread != Thread.currentThread()) {
thread.interrupt();
}
}
}
// catch (TimeoutException e) {
// PExplicitGlobal.setStatus(STATUS.TIMEOUT);
// throw new Exception("TIMEOUT", e);
// }
// catch (MemoutException | OutOfMemoryError e) {
// PExplicitGlobal.setStatus(STATUS.MEMOUT);
// throw new Exception("MEMOUT", e);
// }
catch (BugFoundException e) {


for (Thread thread : threads) {
if (thread != Thread.currentThread()) {
thread.interrupt();
}
}

// (schedulers.get( PExplicitGlobal.getTID_to_localtID().get( Thread.currentThread().getId() ))).updateResult(); // Update result field before setting status

// PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
// PExplicitGlobal.setResult("cex");


PExplicitLogger.logStackTrace(e);

ArrayList<ReplayScheduler> replayers = new ArrayList<>();
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
replayers.add(new ReplayScheduler((schedulers.get(i)).schedule));

ArrayList<Scheduler> localSchedulers = PExplicitGlobal.getSchedulers();
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
localSchedulers.set(i, replayers.get(i));
ReplayScheduler replayer = new ReplayScheduler( e.getBuggySchedule() );

PExplicitGlobal.setRepScheduler(replayer);
PExplicitGlobal.addTotIDtolocaltID(Thread.currentThread().getId(), e.getBuggyLocalTID());

try {
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
(replayers.get(i)).run();
replayer.run();
} catch (NullPointerException | StackOverflowError | ClassCastException replayException) {
PExplicitLogger.logStackTrace((Exception) replayException);
throw new BugFoundException(replayException.getMessage(), replayException);
} catch (BugFoundException replayException) {
PExplicitLogger.logStackTrace(replayException);
PExplicitLogger.logStackTrace(replayException); // This should be throw exception again!
throw replayException;
} catch (Exception replayException) {
PExplicitLogger.logStackTrace(replayException);
throw new Exception("Error when replaying the bug", replayException);
}
throw new Exception("Failed to replay bug", e);
} catch (InterruptedException e) {
PExplicitGlobal.setStatus(STATUS.INTERRUPTED);
throw new Exception("INTERRUPTED", e);
} catch (RuntimeException e) {
PExplicitGlobal.setStatus(STATUS.ERROR);
throw new Exception("ERROR", e);
} finally {
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
Future<Integer> future = futures.get(i);
future.cancel(true);
}
// catch (InterruptedException e) {
// PExplicitGlobal.setStatus(STATUS.INTERRUPTED);
// throw new Exception("INTERRUPTED", e);
// }
// catch (RuntimeException e) {
// PExplicitGlobal.setStatus(STATUS.ERROR);
// throw new Exception("ERROR", e);
// }
finally {
executor.shutdownNow(); // forcibly shutdown EVERY thread

Boolean isMemOutException = false;
Boolean NoException = true;
Boolean isBugFoundException = false;
Boolean AllTimeOutException = true;
int buggyScheduleIndex = -1;
int memOutScheduleIndex = -1;

for (int i = 0; i < timedCalls.size() ; i++) {
Throwable ePerThread = (timedCalls.get(i)).getExceptionThrown();
if (ePerThread != null && !(ePerThread instanceof InterruptedException))
/* Interrupted exception is thrown because 'sleep' of other threads is interrupted somewhere - possibly by timeout feature
or blocking on no current jobs available, so dont want this to go into `etc error case' */
NoException = false;
if (!(ePerThread instanceof TimeoutException))
AllTimeOutException = false;
if (ePerThread instanceof MemoutException || ePerThread instanceof OutOfMemoryError) {
isMemOutException = true;
memOutScheduleIndex = i;
}
else if ( ePerThread instanceof BugFoundException) {
isBugFoundException = true;
buggyScheduleIndex = i;
}
}

if (NoException) { // Correct Case (all threads report correct)
PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS);
PExplicitGlobal.setResult("Correct");
printStats();
PExplicitLogger.logEndOfRun(schedulers.get(0), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds()); // PIN:
}
else if (isMemOutException) { // Memory Error (atleast one thread throws MemOut Exception)
PExplicitGlobal.setStatus(STATUS.MEMOUT);
PExplicitGlobal.setResult("MemOut");
printStats();
PExplicitLogger.logEndOfRun(schedulers.get(memOutScheduleIndex), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
throw new Exception("MEMOUT");
}
else if (isBugFoundException) { // Bug Found Exception (atleast one thread throws BugFound Exception AND no thread throws MemOut Exception)
PExplicitGlobal.setStatus(STATUS.BUG_FOUND);
PExplicitGlobal.setResult("cex");
printStats();
PExplicitLogger.logEndOfRun(schedulers.get(buggyScheduleIndex), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
throw new BugFoundException();
}
executor.shutdownNow();
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
(schedulers.get(i)).updateResult();
printStats();
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++)
PExplicitLogger.logEndOfRun(schedulers.get(i), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
else if (AllTimeOutException) { // All threads timeout
PExplicitGlobal.setStatus(STATUS.TIMEOUT);
PExplicitGlobal.setResult("TimeOut");
printStats();
PExplicitLogger.logEndOfRun(schedulers.get(0), Duration.between(TimeMonitor.getStart(), Instant.now()).getSeconds());
throw new Exception("TIMEOUT");
}
else { // Some other case
PExplicitGlobal.setStatus(STATUS.ERROR);
PExplicitGlobal.setResult("error");
printStats();
throw new Exception("ERROR");
}

}
}

public static void run() throws Exception {
ArrayList<Scheduler> localSchedulers = PExplicitGlobal.getSchedulers();
for (int i = 0; i < PExplicitGlobal.getMaxThreads(); i++) {
ExplicitSearchScheduler localCopy = new ExplicitSearchScheduler();
schedulers.add(localCopy);
localSchedulers.add(localCopy);
}


preprocess();


process(false);


}

}
4 changes: 2 additions & 2 deletions Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/commandline/PExplicitConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
public class PExplicitConfig {
@Getter
@Setter
private static int numThreads = 1;
private static int numThreads = 4;
// default name of the test driver
final String testDriverDefault = "DefaultImpl";
// name of the test driver
Expand All @@ -36,7 +36,7 @@ public class PExplicitConfig {
int verbosity = 0;
// max number of schedules bound provided by the user
@Setter
int maxSchedules = 1;
int maxSchedules = 4;
// max steps/depth bound provided by the user
@Setter
int maxStepBound = 10000;
Expand Down
Loading

0 comments on commit 419f335

Please sign in to comment.