Slow Petri Net Unfolding (the Bumblebee Observations)

[Heizmann]

The Petri net unfolding is at the moment (early Oct 2019) the major bottleneck of the Petri Automizer verifier. The Petri net unfolding seems to be unnecessarily slow.

The following list of observations should help us to discuss improvements.

The Dinosaur Observations:

• D01: Typically, we have dozens of conditions per place.
• D02: Only few candidate for possible extension finally evolve to a possible extension
• D03: >90% CPU time is spend for checking if two conditions are in co-relation, but the implementation of this check is efficient

The Bumblebee Observations:

• B01: We instantiate conditions in candidates incrementally, approx 10% of the initial 1-condition instantiated candidates finally evolve to at least one possible extension.
• B02: While evolving a candidate we try to instantiate places with conditions and iterate over all conditions (dozens, see D01) that have a certain place.
• B03: Because of B02 the high cost are probably not due to the high number of the 1-condition instantiated candidates but due to the high costs for evolving a candidate.
• B04: Many instantiations fail because the condition is successor of a cut-off event.
• B05: The datastructures of the ConditionEventsCoRelation would allow us to get all conditions that are in co-relation to a given condition c. The number of all co-related conditions is typically high. Iterating over all of them is not efficient.
• B06: These datastructures would not allow us to get all conditions that are in co-relation to a given condition c and have a certain place p.
• B07: The B06 problem can be addressed: Do not store binary condition->event relation, but ternary condition->transition->event relation. Given condition c and place p, when asked for {c'| c' in co-relation to c and has place p} then find all predecessor transitions of p (separate tracking necessary, Petri nets only provide forward successors) get co-related event and filter successors for places.
• B08: We could save even more if we omit cut-offs from co-relation.
  Check with other users (backfolding, LBE) if this could become the default.
• B09: Memory optimization for internal data structure: We store for each condition the co-related events. Idea: Store the information only for the parent event (is a subset) and only the remaining diff for the condition.
  Saves probably also runtime because we have to copy fewer relations. Makes implementation more complex. (Probably wait until this becomes a bottleneck)
• B10: We could use co-relation information to reduce the number of 1-condition instantiated candidates in the first place.
  Orthogonal to B07. Requires additional callbacks for the on-demand construction. Makes implementation significantly more complex. Do not implement until this becomes the dominant bottleneck of the algorithm.

[Heizmann]

• B11: The method BranchingProcess#isOneSafe is also very costly. If we trust the input to be 1-safe. Otherwise we could check 1-safety more efficiently by checking that each place occurs at most once in each local configuration.

[Heizmann]

For benchmarks on the set above,
CONDITION_PER_PLACE_MAX is between 90 and 25000, and
CO_RELATION_MAX_DEGREE is between 3000 and 70000.
CsvAutomataOperationStatistics107285100_2019-10-13_14-33-48-842.csv.txt
java.hprof.txt
The total runtime of the subTwoHourMarathon subset is 763s.

[Heizmann]

For the benchmarks in the set above:
ae0a586 sped up the unfolding for larger benchmarks by factor 3 and reduced co-relation queries by up to 40%.
(@naouarmehdi unfortunately, a side-effect is that benchmarks done before and after this commit are not comparable wrt. number of co-relation queries.)
CsvAutomataOperationStatistics107285100_2019-10-13_14-57-02-088.csv.txt
java.hprof.txt
The total runtime of the subTwoHourMarathon subset is 310s.

[Heizmann]

• B12: If we run the verification on larger examples, timeouts occur almost always in these FinitePrefix operations that are applied to a DifferencePairwiseOnDemand. These operation is done in order to enhance the Floyd-Hoare automaton on-demand (constructing the Floyd-Hoare automaton eagerly is no alternative for large programs).

[Heizmann]

• B13: The subTwoHourMarathon subset is more relevant for program verification than the other four benchmarks in the set. It seems that we have different bottlenecks for both sets.
  The hprof output is dominated by the four more time-consuming but less important benchmarks.