Skip to content

Latest commit

 

History

History
139 lines (111 loc) · 8.12 KB

changelog-2018.md

File metadata and controls

139 lines (111 loc) · 8.12 KB
Raw

Changelog for 2018

2018-12-31

  • 🔄 Default depth limit for DfsBProgramVerifier raised from 100 to 1000.
  • ✨ Deadlock detection prints deadlock details: for each event, who requested it, and who blocked it.
  • ✨ New verification switch: --liveness checks for liveness properties only.

2018-12-26

  • 🐛 Fixed an off-by-one error in the state count of the DFS verifier. Also, cleaned up some of its design.
  • ✨ More tests
  • 🚮 Cleanup of DfsBProgramVerifier.

2018-12-24

  • ✨ Removed dependencies (closes #69)
  • 🔄 Using a fixed thread pool, rather than a cached one (so preventing cases where too many threads from running at once).
  • 🐛 Fixed a HUGE memory leak. Huge.
  • 🐛 Fixed a crash in PrioritizedBThreadsEventSelectionStrategy when all the events were blocked (#70).
  • ✨ More tests
  • ✨ Cleanups
  • 🚮 Setting interrupt handlers, the last BPjs task that was not under bp object, is now a bp method. So setInterruptHandler is now bp.setInterruptHandler.

2018-12-23

  • 🚮 BProgram cannot evaluate resources anymore. This change also removes this ability from running JavaScript b-program. It made no sense anyway, and was not used.
  • ✨ SingleResourceBProgram can now accept multiple resources, and was thus renamed to ResourceBProgram (#60). (NOTE: this change breaks program that gave explicit names to a SingleResourceBProgram in the constructor, as the argument for the name is now interpreted as a resource name. You can use setName to set the program name later.
  • ✨ Automatic event names include the name of the class and an index number.
  • 🐛 Fixed broken links in the documentation.
  • ⬆️ Improved Javadocs.

2018-12-19

  • ✨ There are two different hot cycle violation inspections: one inspects a hot loop at the b-thread level (default), and the other at the whole b-program level.
  • ⬆️ More tests.
  • ✨ Updated the docs to reflect the updates in verification features.

2018-12-15

  • ✨ More verification package updates: now differing between cycle inspections and trace inspections.
  • ✨ Detection of hot cycles. That is, we can verify liveness requirements. 🎉 🎉 🎉
  • ⬆️ Better hash function for BThreadSycSnapshot.

2018-12-15

  • ✨ Verification area gets some well-needed refactoring:
    • Inspections get their own interface (so it's easier to add new ones)
    • Common inspections no live in the DfsVerificationInspections utility class.
    • The violations part of VerificationResult moved into Violation class. This allows much cleaner code for inspecting violation as as an open infrastructure for detecting new types of violations (#61).
  • ⬆️ External Events are now part of the equals method of BProgramSyncSnapshot.

2018-12-14

  • 🔄 Renamed BSyncStatement to SyncStatement, as we don't call it "bsync" anymore. Also updated the toString method, which still used the pre-historic RWBStatement term.
  • ✨ SyncStatements can now be "hot".
  • ⬆️ Improvements to BProgram's API.

2018-11-25

  • ✨ fork() added (#57).

2018-11-23

  • 🐛 Fixed scope issues with b-thread continuations.
  • ✨ Validated scope unit tests are passing.

2018-11-20

  • ✨ more tests, re: dynamic b-thread addition
  • ✨ added Devoxx.be2018 talk 🎉
  • 🚮 code cleanup

2018-10-17

  • ✨ BProgramRunner now has a halt() method #53.
  • ✨ Documentation now covering verification (well, the basics).
  • ✨ A b-progrm's logging level can be set from Java (#50)
  • 🚮 Removed old exception code. More tests.
  • 🚮 bsync, deprecated long ago, was removed.

2018-10-16

  • 🔄 ambiguous term daemonMode changed to waitForExternalEvents (#54).
  • 🐛 PrioritizedBSyncEventSelectionStrategy selected wrong event.

2018-10-20

  • ✨ BPJsCliRunner can now directly executed from Maven, using mvn exec:java. Pass arguments using -Dexec.args="args go here".
  • ✨ BPJsCliRunner can verify a program. Pass --verify as a commandline argument. Use --full-state-storage to force the verification to use the full state data when determining whether a state was visited (requires more memory).

2018-10-13

  • 🐛 B-Program setup sequence is consistent for all b-threads, including those in appended code.

2018-08-08

  • ✨ Decorating event selection strategies just go easier with the introduction of AbstractEventSelectionStrategyDecorator.
  • ✨ Added a pausing event selection strategy, to allow pausing and rate-limiting the execution of a BProgram.
  • 🐛 PrioritizedBSyncEventSelectionStrategy deals with its own JavaScript Context properly (fixes #34).
  • ✨ Added a "what do you want to do" section to the docs, to help newcomers.

2108-06-*

  • ✨ Many more tests and benchmarks.

2018-04-26

  • 🐛 Verifiers can be re-used.
  • ✨ Support for modern JS features, such as let expressions and generators.
  • ✨ bp.sync prints a warning when a b-thread blocks an event it requests #10.
  • 🚮 Removed extra logging.
  • ⬆️ More tests.
  • ⬆️ Fixed TicTacToe example: now split into two executing classes (interactive GUI and verification). Same core TTT code is used in both, which proves the point that BPjs can be used for smooth transition from verified model to a full application. 🎉
  • ✨ Added a file with useful tips.
  • ✨ MOAR UNIT TESTSTSSSTTTSTSS!!!!!!!

2018-03-21

  • ✨ bsync is deprecated, in favor of bp.sync. The latter can be called from any function, not just the immediate b-thread function.
  • ✨ BProgramRunner now implements Java's Runnable.
  • ⬆️ Simplified b-thread scope processing. This means scopes behave closer to what a JavaScript programmer would expect.
  • ⬆️ Javadoc references use latest version (rather than a fixed one).
  • 🔄 Code cleanup.
  • 🔄 Documentation cleanup.
  • 🔄 Old updates from this file moved to "changelog" files.

2018-02-25

  • ⬆️ VisitedStateStore Adds a clear() method.
  • 🐛 DfsBProgramVerifier instances can now be re-used.

2018-01-24

  • ⬆️ 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.

2018-01-18

  • 🐛 Fixed a crash where program with failed assertions were intermittently crashing.

2018-01-17

  • 🐛 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).

2018-01-12

  • 🐛 ✨ Refactored analysis code, removing the invalid (easy to understand, but invalid) PathRequirement based 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.

2018-01-11

  • ✨ 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).

Earlier Changes