jcp19 / spider

Automated data race detection from a distributed trace via SMT constraint solving

Hello World! 👋🌎

• ❤️ Formal Methods, Programming Languages, Concurrency, Distributed Systems
• 🔭 Ph.D. student in the Programming Methodology Group at ETH Zürich
• 📫 Check my website for contact info

spider's Issues

Refactor references to minha-checker, change the project name to Spider

Remove occurrences of minha-checker throughout the repo. Change the name of the repo and change the path to the src files.

Tests lacking

There's no testing in this project. I believe the best way to do this will be to run the program with small instances of traces and compare it's results to results computed 'by hand'. Besides, I believe this project could gain from having some unit testing.

Test scripts hard to mantain

The couple of scripts in the repository are probably outdated and are unnecessarily convoluted. It is better to create a small class to test the program and generate the reports. At first sight, it looks like it is going to need some hacks because the TraceProcessor class is a singleton -.-

Confusing result reporting

Improve the output of the program. The current output has a bunch of debug information which should not be printed.

Is the current way to count the number of actual data races the right way to do it?

Check if the data race candidates are actually a pair of locations in the code. That is the only way to ensure that each data race candidate is counted only once.

Removing Inter-Thread Event Redundancy is leading to races being missed

In the case of the m3274.log in traces/micro-benchmarks, the number of detected data race conditions drops from 3 to 1 when the removing "redundant" inter-thread events. At first, it seems like a bug in the elimination of SND and RCV events but need more testing.

If this happens to not be a bug and the the removal of messages is proven to be unsound, we can create a new flag for Spider (-E) which stands for "Experimental Redundancy Elimination"
which will call the extension on ReX.

Debug all structures in falcon used for the hb-model generation

Debug all other structures in TraceProcessor to make sure that they are properly populated.
Even a small bug in TraceProcessor can have a big consequence on our results (e.g. fntneves/falcon#43)

To much reliance on System.out instead of log files

Big use of System.out.println instead of adequate use of log.debug and log.info

Add FindBugs to pom.xml

Improve `Stats` Class

Ideas:

• align results in the output
• convert this class to a singleton instead of using static fields

Old README

Improve description of the project, its goals, dependencies, how to install it and how to use it.

Simplify evaluation scripts

Instead of having two different gawk scripts for each of the two evaluation scenarios (data race detection and message race detection), I believe that one suffices per scenario. The gawk script should accept and argument detailing which of the two csv formats to print and read in the END action. In the body, we should read every required line/argument

Example traces are outdated and not compatible with the new version of Falcon.

Hidden Dependency between RaceDetector and Z3SolverParallel

The constructor of RaceDetector receives a Solver as an argument. However, this Solver is eventually casted to a Z3SolverParallel. In this case, I think it is better to make the dependency in the constructor.

Debug results for the Cyclon trace

Current results without elimination:

 > Data Race #1 : (cyclonlite.CyclonActive.initWithData.73, cyclonlite.CyclonActive.insertReceivedToView.198)
 > Data Race #2 : (cyclonlite.CyclonActive.initWithData.73, cyclonlite.CyclonActive.selectPeersToShuffle.249)
 > Data Race #3 : (cyclonlite.CyclonActive.insertReceivedToView.198, cyclonlite.CyclonActive.selectPeersToShuffle.249)

The first two races should not happen

Add continuous integration to run tests and detect code style violations

Optimization possible

Basically, the races seem to be very "local" in the sense that even though they have hundreds of candidates, what happens, at least in the case of the cyclon, is that these races translate into a few unique locations. Therefore, a possible optimization would be to make a list of unique possible locations in race from the set of candidates to race conditions and then only solve until you find a race. All other candidates can be ignored because even if they are sat, they will give rise to a race that has already been detected