Streamlining

Minor changes, streamlining the APIs.

ComposableEventSet, re-composed

Main feature for this release - the old ComposableEventSet class, which worked for runtime but did not play well with verification, now works with verification too. And also has some basic boolean semantic functionality:

These are equal:

theEventSet(E_A).or(E_B).and( theEventSet(E_B).or(E_C) )
theEventSet(E_C).or(E_B).and( theEventSet(E_B).or(E_A) )

These are equal:

allOf(E_A, E_B, E_C, E_D)
allOf(E_A, E_B).and(allOf(E_C, E_D))
allOf(E_A, E_B, E_B, E_B).and(allOf(E_C, E_D));

State Space Travel

DFSBProgramVerifier can now continue to traverse the program state space AFTER it has found a violation. This allows detecting multiple violations, pruning, and performing other explorations of a b-programs' state space.

Also, various improvements, especially regarding hashing functions of BProgramSyncSnapshots, and the objects that compose them.

Now, also working in theory

This version of BPjs is informed by requirements from users of the verification functionality. It is much more aligned with theory behind BP. For example, event selection strategies accept a state of a b-program as a parameter, when they have to select and event (as opposed to a set of synchronization statements).

The verification area has been refactored towards re-use: execution traces no longer assume they were created by the DFS verifier, trace inspections (deadlock detections etc.) can accept any execution trace.

Other notable changes:

• Improved testing infrastructure for verification and analysis (e.g. mock b-program states)
• Improved hashing algorithm for BProgramSyncSnapshots
• More tests
• Code and documentation cleanups.

Bugfixes - verification edition

Fixes some bugs in state comparison. These led to false negatives, where the verifies did not detect that it has already visited a state.
Also, much improved hashing algorithm for program states, especially in cases where JavaScript objects are used as data in events.

Bugfixes

Biggest news for this release:

• Fix of a longstanding memory leak that prevented BPjs from running for a long time.
• Removed dependency on commons-lang.
• Other bugs were fixed as well.
• Also some code cleanup, and more tests.

Minor breaking change: Setting interrupt handlers is now done using bp.setInterruptHandler, rather than by calling setInterruptHandler on a b-thread specific context.

It's ALIVEness

BPjs is now able to verify liveness properties, by marking sync points as "hot" (yes, that terminology is a tip of the hat to LSC's). BPjs can detect overall hot cycles (an infinite loop where a b-program, as a whole, must always advance even without external events) and b-thread specific cycles (where a b-thread is in an infinite loop where all it's sync points are "hot").

Also:

• Verification re-designed, so now it's possible to add new inspections and report new violations
• Easier to create a BProgram from multiple resources (based on actual user feedback!)
• BEvent sub classes assign a meaningful name by default to their instances (based on actual user feedback!!)
• Improvements to the documentation (both high-level and Javadocs, based on actual user feedback!!!).
• More tests (now over 81% coverage!*)

* We of course acknowledge that coverage itself is not enough, which is why we bother with verification in the first place. But it's not entirely useless either.

Forkin'

• C-like fork() (split the b-thread at the call site, on the child returns true and on the parent false)
• Fixed scope issues with starting b-threads
• More tests - tests that were skipped before due to time/ambiguity are now fixed and executed in full.

🍴

MODELS18 edition

Honoring our two contributions to MODLES18, this release contains:

• Verification from the command line! (just pass --verify)
• Better API, based on actual usage by actual users (still from BGU's internal group, true, but users nonetheless)
• Code cleanup
• Updated documentation
• and more (see README, as usual).

Decorations and Pauses

1. EventSelectionStrategies are easier to decorate
2. We can pause a running program using PausingEventSelectionStrategyDecorater (assuming, of course, you can type this). See example of rate limiting a BProgram here: https://github.com/bThink-BGU/BPjs/blob/develop/src/test/java/il/ac/bgu/cs/bp/bpjs/model/eventselection/PausingEventSelectionStrategyDecoratorTest.java
3. Many more tests
4. Bug fixes