This repository contains a javascript-based BP library.
- BPjs is open sourced under the MIT license. If you use it in a system, please provide a link to this page somewhere in the documentation/system about section.
- BPjs uses the Mozilla Rhino Javascript engine. Project page and source code can be found here.
- For Maven projects: Add BPjs as dependency. Note that the version number changes.
<dependencies>
...
<dependency>
<groupId>com.github.bthink-bgu</groupId>
<artifactId>BPjs</artifactId>
<version>0.8.6</version>
</dependency>
...
</dependencies>
- Clone, fork, or download the starting project.
- Download the
.jarfiles directly from Maven Central. - The project's Google group
- Presentations: Introduction Deeper dive
- Tutorial and Reference
- API Javadocs
- โฌ๏ธ
VisitedStateStoreAdds aclear()method. - ๐
DfsBProgramVerifierinstances can now be re-used.
- โฌ๏ธ Improved hashing algorithm on
BThreadStateVisitedNodeStore. - โจ Transient caching of thread state in
BThreadSyncSnapshots. This improves verification performance, with low memory cost. - ๐ Removed visited state stores that took incoming state into consideration.
- ๐ More mazes in the Mazes example.
- ๐ Fixed a crash where program with failed assertions were intermittently crashing.
- ๐ Verifier now correctly identifies deadlock as a state where there are requested events, but they are all blocked (formerly it just looked for the existence of b-threads).
- ๐ โจ Refactored analysis code, removing the invalid (easy to understand, but invalid)
PathRequirementbased analysis, and using only b-thread now. This design is much cleaner, as it uses less concepts. Also moves us towards "everything is a b-thread" world. - โจ Added tests to demonstrate the various states a verification can end in.
- ๐ Verifiers and runners terminate their threadpools when they are done using them.
- โจ During forward execution, b-threads can halt execution using
bp.ASSERT(boolean, text). - โฌ๏ธ Refactored the engine tasks to support raising assertions. Reduced some code duplication in the way.
- โฌ๏ธ Thread pools executing b-threads are now allocated per-executor/verifier (as opposed to using a single static pool).
- โฌ๏ธ Re-arranged package structure, duplicate and ambiguous packages merged. We now have a clean
model/execution/analysisdivision. - ๐ Fixed an equality bug in
OrderedSet.
- ๐
BSyncStatements now retain information about the b-thread that created them. - โฌ๏ธ Now using a single
ExecutorServicefor the entire JVM (OK, per class-loader). This makes runtime more efficient, resource-wise. - ๐ Using cached thread execution pool instead of the fork-join one (the former seems to make more sense in a BP context).
- โฌ๏ธ The Java threads executing the b-threads now have specific names:
bpjs-executor-N(whereNis a number starting at 1). - โจ New method:
bp.getJavaThreadName: Returns the name of the Java thread executing the b-thread while this method was called. - ๐ Some changes in this version were requested by actual users. ๐
- โจ Documentation updated to mention verification (full-length text to be added post-paper).
- ๐
BThreadJSProxy.get/setBthreadupdated to use capitalT, like the resp fo the code. - ๐ Test clean-up
- ๐ Documentation clean-up
- โจ
BProgramallows appending and prepending source code programmatically, usingappendSourceandprependSource. These can be used to add environment simulation without touching the simulated model. Or just to act as includes, e.g. for common set-ups. - โจ Added new class:
PathRequirements, to hold path requirements that do not require state (e.g. "no deadlock"). - โจ
DfsBProgramVerifiernow has a "debug mode" (set/get viaget/isDebugMode). On debug mode, it prints verbose information toSystem.out. - โจ Added new class:
BThreadStateVisitedNodeStore, looks only into the states of the b-threads when deciding whether a search node was already visited or not. - ๐
InMemoryEventLoggingListenercleans its event log when a run begins, so it can be reused for multiple runs. - ๐ Reduced method accessibility in
BProgram, so subclassers have harder time getting into trouble. - :put_trash_in_its_place:
BProgramListenerrenamed toBProgramRunnerListener, since that is the object it listens to. - :put_trash_in_its_place:
NoDeadlockclass deleted. UsePathRequirements.NO_DEADLOCKinstead. - โจ
PathRequirements.ACCEPT_ALL, is a new requirement that's always true. Useful for scanning a program state space.
- โฌ๏ธ
DfsProgramVerifierusesFullVisitedNodeStoreby default (preferring correctness over speed in the default case). - โฌ๏ธ Updated the Dining Philosopher example to use advanced features. Also added it as a unit test.
- ๐ฎ Removed
validationpackage. - โจ
ContinuationProgramStatecorrectly captures updated variable values. ๐
- โจ the
DfsBProgramVerifieris now accepting requirement objects over execution paths, instead of the hard-coded deadlock check. - โจ new
PathRequirementclass. Requirements are passed to the verifiers for making sure the program conforms to them. Two implementation already present:NoDeadlockBreakes when there's a deadlockEventNotPresentBreaks when the last event in the ongoing path is a member of a given event set.
- โจ the
DfsBProgramVerifieris now using listener architecture for reporting progress. - โจ new event set from bp:
bp.allExcept(es). - โฌ๏ธ Efficient path stack implementation for
BfsBProgramVerifier(no copying, reversal, etc.) - โฌ๏ธ
Mazes.javaUpdates to fully use the new verifier features
- โฌ๏ธ Re-created program state cloning based on code from @szegedi. Cloning is now faster, more efficient, and can handle storage of events.
- โจ New base class for implementing event selection strategies.
- โจ
OrderedEventSelectionStrategy- A new event selection strategy that honors the order in which events are requested by a given b-thread. - โจ
PrioritizedBThreadsEventSelectionStrategy- A new event selection strategy that can assign priorities to b-threads. - โจ
PrioritizedBSyncEventSelectionStrategy- A new event selection strategy that allows b-threads to add priority to theirbsyncs. - โฌ๏ธ
LoggingEventSelectionStrategyDecoratoralso logs selectable events - โฌ๏ธ
BProgramacts nicer when it has anullevent selection strategy.
- โจ Updated to Rhino 1.7.7.2.
- โจ Initial verification added.
DfsBProgramVerifierscans the states of aBProgramusing DFS, and can return traces where there are no selectable events.
- โจ Added a class to compare continuations (base for comparing snapshots).
- โจ
bsyncnow has an extra parameter, allowing b-threads to pass hinting data to customEventSelectionStrategys. - ๐ Moved event selection strategy to
BProgram. - โจ Added a mechanism to log the
BProgramStateat sync points.
- โจ Added documentation for embedding BPjs programs in larger Java apps.
- โจ README includes a more prominent reference to the documentation.
- โจ Added an adapter class for
BProgramListener. - ๐ Fixed issues with adding objects to the program's scope.
- ๐ฎ Cleaned up the
BProgramRunner-BProgram-BProgramSyncSnapshottrio such that listeners don't have to be passed around between them. - โจ Cloning of
BProgramSyncSnapshotready. This is the basis for search.
- โจ New architecture: Running logic moved from
BProgramtoBProgramRunner- ongoing. - โจ
BProgramListeners notified before BPrograms are started. - ๐ Fixed a bug where dynamically added b-threads that were added by other dynamically added b-threads would run one cycle too late.
- ๐ Fixed a bug where external events enqueued from top-level JS code where ignored.
- โจ New architecture: Running logic moved from
BProgramtoBProgramRunner. This will help implementing search. - โจ
BProgramListeners notified when a b-thread runs to completion. - โจ
bp.getTime()added. - โจ Updated tutorial now includes the
bpobject.
- ๐ฎ Simplified the
examplestest package. - ๐ฎ
allandnoneare now only available viabp. - ๐ cleaner scope structure..
- ๐ Internal method name clean-ups.
- ๐ฎ Removed unneeded initializations.
- ๐ Program and bthread scopes are treated as scopes rather than prototypes.
- โจ B-Thread scope games eliminated ๐. Dynamic b-thread addition is now possible from within loops etc. Tutorial updated.
- โจ More tests.
- โจ
bp.randomadded. - ๐ Documentation updates
- โจ Added java accessors for putting and getting variables in the JS program
- ๐
fat.jaris nowuber.jar.
- โจ the standard
.jarfile now contains only BPjs, and no dependencies. Fat jar (the jar that includes dependencies) is available via the releases tab.
- ๐
Eventsclass renamed toEventSets. Some cleanup. - ๐
emptySetis nownone. - ๐
allandemptySetare now available to BPjs code viabp.allandbp.none. This is to prevent name collisions with client code. - ๐ Fixed an issue with the logger, where logging levels were ignored.
- โจ Log level can be set by BPjs code, using
bp.log.setLevel(l).lis one ofWarn,Info,Fine.
- โจ Updated documentation to refer to Maven Central
- ๐
RunFilere-reads files from file system again. - ๐ More dead code removal.
This release in focused on better BPjs-programmer experience and getting the code into a maven-central quality grade.
- ๐ Fixing Javadoc references.
- ๐ฎ Positional
bsyncremoved. - โจ Better error reporting on event sets defined in JavaScript.
- โจ Better error reports for generic JS errors.
- โจ Added
StringBProgram: a new class for running BPjs code from a String (rather than a resource or a file).
- โจ Adding a BThread is idempotent. Previously, if a BThread was added twice, it would run twice with unexpected results.
- โจ Basic engine exceptions, plus a friendlier error message when calling
bsyncoutside of a BThread. - ๐ More Javadocs and code cleanup (mostly dead code removal).
- โจ License (MIT)
- โจ Preparations for Maven Central
- ๐ More Javadocs and code cleanup.
- โจ
RunFilecan now accept multiple BPjs files for input, and runs them as a single BProgram. It also has improved help text.
- โจ Added continuous code coverage with Coveralls.io (Thanks guys!).
- โจ Improved test coverage.
- โจ Added continuous testing with Travis-CI (Thanks guys!).
- ๐ Moved from native NetBeans to maven project ๐ ๐ โจ
- ๐ Various small issues fixed thanks to static analysis (and NetBeans' Code Inspection tool).
- ๐ Moved to canonical package structure (
il.ac.bgu.cs.bp.*).
- โจ Re-arranged code to minimize amount of
Context.enter-Context.exitpairs (~x5 performance factor!) - โจ Simplified mechanism for handling event selection in
BProgram. Replaced a complex Visitor pattern with Java8'sOptional. - ๐ Improved efficiency for external events handling.
- โจ More tests for
SimpleEventSelectionStrategy. - โจ More documentation.
- โจ Better error messages.
- ๐ฎ Removed unused code from
BProgram. - ๐ฎ Removed non-serializable
Optionalfrom fields.
- ๐ฎ Removed
bpjsfrom JS scope. Programs must usebpnow. - ๐ฎ Polished the interface for adding BThreads to a program: 1 method instead of 3.
- ๐ Fixed an issue where external events were re-ordered while checking for daemon mode termination.
- ๐ A BProgram now quits when there are no more BThreads, even if there are enqueued external events.
- ๐ Fixed typos in error messages.
- ๐ Reduces method accessibility to minimum (nothing is
publicunless it has to be). - โจ More documentation.
- โจ A class for running bpjs files.
- ๐ Efficient use of
Context, so that we don't open and exit it all the time. - ๐ฎ More removal of more unused code. We now have less unused code. Less is more, especially with unused code.
- ๐
breakUponis nowinterrupt. This leavesbreakUponto be later used as a language construct rather than absyncparameter.
- ๐ฎ โจ ๐ Big refactoring and clean-up towards enabling search.
BThreads removed from engine - main new concept is that an execution of a BThread is a series ofBThreadSyncSnapshot, advanced/connected byBPEngineTasks. A BProgram is an execution environment for multiple BThreads (plus some state and management code).
- ๐
breakUponhandlers are evaluated in theBThread's context, rather than in theBProgramone.
- โจ Updated the logging mechanism from global, single level to 3-level. Code change required:
bplog("hello") -> bp.log.info("hello). Also supportswarnandfine. - ๐ฎ
bpjsis deprecated (but still works). Please usebpnow. - ๐ฎ positional bsync deprecated (but still works). Please use the named-argument variant
bsync({request:....}). - ๐ฎ BThread is not exposed in Javascript via
bt(that was never used). - โจ BThreads can now enqueue external events using
bp.enqueueExternalEvent(). - โจ BThreads can now specify a function that will be executed if they are removed because an event in their
breakUponevent set was selected. UsesetBreakUponHandler( function(event){...} ).
- โจ Restructured the engine with JS proxies - javascript code has no direct interaction with the Java engine parts!
- ๐ More unit tests and examples
- Restructured the engine with JS proxies - javascript code has no direct interaction with the Java engine parts!
- More unit tests and examples
-
โจ BEvents now have an associated
dataobject. See example here -
โจ New way of creating
BEvents: a static method namednamed:new BEvent("1stEvent") // old BEvent.named("1stEvent") // new and English-like.
Future usaged include the ability to reuse event instances, but we're not there yet.
-
โจ Added support for Javascript definition of event sets:
var sampleSet = bpjs.EventSet( function(e){ return e.getName().startsWith("1st"); } );
-
โจ Support for
breakUponinbsyncs:bsync( {request:A, waitFor:B, block:C, breakUpon:D})
-
โจ
SingleResourceBProgram- a convenience class for the common case of having a BProgram that consists of a single file.
- ๐ BProgram's
setupProgramScopegets a scope as parameter. So no need to callgetGlobalScope, and it's clearer what to do. - โจ
RWBStatementnow knows which BThread instantiated it - โจ When a program deadlock,
StreamLoggerListenerwould print theRWBStatements of allBThreads.
Legend:
- ๐ Change
- โจNew feature
- ๐ฎ Deprecation
- โฌ๏ธ Upgrade
- ๐ Bug fix
