UnderstandingTheMachine

Strategy

The main strategy of AProVE is located at aprove.predefinedstrategies.Auto.current.strategy. It is a very basic, grammar-like, self-explanatory file.

Defined Strategies

Strategies are denoted by lower-case words, like trs. Defining such a strategy simply means defining the following equation: trs = ..., where on the right-hand side of the equation you can now define what processors to use. Processors are denoted by upper-case words, like TRSToQTRS. In the std.strategy file (located at aprove.predefinedstrategies.Modules.std.strategy) you can find a dictionary relating processor classes to their corresponding name in the strategy file, like declare TRSToQTRS = aprove.verification.theoremprover.TerminationProcedures.TRSToQTRSProcessor. By using additional primitives in the strategy, we can describe repeating a processor a certain amount of time, performing two processors in parallel, etc.

Strategy Primitives

The following is a list of all strategy primitives with their corresponding meaning. It is stated that all of them should be self-explanatory.

• 'Any' This strategy executes several sub-strategies one by one in parallel and continues until it receives a Success(...) result from one of them.
• 'First' This strategy executes several sub-strategies one by one sequentially (in chronological order) and continues until it receives a Success(...) result from one of them.
• 'Repeat' This strategy repeats a sub-strategy a specific amount of times (or even infinitely often, denoted by a '*') until it receives a Success(...) result in some iteration. Works in parallel if multiple new obligations are produced.
• 'RepeatS' This strategy repeats a sub-strategy a specific amount of times (or even infinitely often, denoted by a '*') until it receives a Success(...) result in some iteration. Works sequentially if multiple new obligations are produced.
• ';' This simply denotes first performing the strategy defined on the left, and if successful moving on with the remaining strategy on the right. If several obligations result from the strategy defined on the left (e.g., QDPDependencyGraph), the strategy on the right will be run in parallel on the obligations rather than sequentially.
• ':' This simply denotes first performing the strategy defined on the left, and if successful moving on with the remaining strategy on the right. If several obligations result from the strategy defined on the left (e.g., QDPDependencyGraph), the strategy on the right will be run in sequentially on the obligations rather than in parallel.
• 'Timer' Has two arguments. The first argument indicates the duration in milliseconds of CPU time that the strategy given as the second argument is allowed to run. If the time limit is reached, the strategy results in Fail, otherwise the result of the strategy given as the second argument is used.
• 'WallTimer' Has two arguments. The first argument indicates the duration in milliseconds of wall time that the strategy given as the second argument is allowed to run. If the time limit is reached, the strategy results in Fail, otherwise the result of the strategy given as the second argument is used.
• 'Maybe' Has one argument, the strategy that is supposed to be run. 'Maybe(someStrategy)' is a shorthand for 'Repeat(0, 1, someStrategy)'.

Basic Constructs in the Framework

The framework understands three basic constructs:

• Success(...): "We're done here, continue work on this".
• Fail: "Something didn't work out".
• Other ExecutableStrategies: Points to more tasks that need to be done.

Once we have a final proof tree constructed, we only then focus on "YES/NO/MAYBE". During the analysis we deal entirely with "stuff to be done". This abstraction allows us to keep things flexible, as the proof tree is the only entity that understands Implications and tracks AND/OR relations. It is the only component that can interpret truth values properly.

The Machine

The Machine is responsible for managing the execution of strategies and processing them in an orderly manner. It holds a reference to an ExecutableStrategy object, which is the interface implemented by every strategy primitive. The basic flow of execution can be described as follows:

How the Execution Works

The exec() method of the strategy works on the principle that:

• If there is no more work to do, return null.
• If there is still work to be done, return a new ExecutableStrategy object (which may be the same strategy, i.e., this, if it needs to execute again).

It may seem unusual that an ExecutableStrategy can return itself (this) to immediately execute again, but this simplifies the implementation of strategy primitives (such as ExecRepeat).

Processors are initiated in separate threads by the ExecProcessorStrategy. When the processor finishes, the machine thread is woken up, traverses the entire strategy execution tree, and continues the process. The result (ObligationNode, Implication, Proof) is grafted into the proof tree, and the strategy part of the result is returned.

Challenges and Limitations

There are some subtle bugs, inefficiencies, and potential performance losses that arise at the strategy level. For example:

• Fail: While we see the Fail result at the strategy level, we do not know what its impact is on the proof tree.
  • If a specific BasicObligationNode cannot be solved, does that mean we are entirely stuck, or does it simply mean we can’t prove termination, but might still prove non-termination, or vice versa?
  • The answer depends on the structure of the proof tree above the node, and it is not always straightforward.

Understanding Solve()

One of the few primitives that actually looks at the proof tree is Solve(). It filters the results based on the truth value of the ObligationNode:

• Solve() returns Success only when the input ObligationNode has been assigned a truth value of YES or NO.
• If Solve() encounters a Success(...) with more work left to be done, or a Success() that doesn't produce a usable truth value (possibly due to unfavorable implications), it will turn into Fail.

Proof Tree Threading Rules

ObligationNode, BasicObligationNode, and JunctorObligationNode (in aprove.prooftree.Obligations) are not thread-safe for concurrent writes. The synchronization present in those classes only prevents readers from seeing inconsistent state — it does not make concurrent modification safe and does not guarantee freedom from deadlocks.

The rule is:

• You may read from any ObligationNode in any thread at any time.
• You may write to a node (e.g. add children) freely, as long as it has not yet been attached to the main proof tree.
• Once a node has been attached to the main proof tree, it may only be modified from the Machine thread — which happens via ExecResult.exec().

Violating this rule (modifying an attached node from a processor thread) can cause race conditions that are very difficult to debug.

Note on Timers and Abortion

When a processor thread is aborted (due to a timeout or manual abortion), it is given a grace period of 5000 milliseconds before it is forcibly killed. This delay serves one purpose:

• Prevent interference: It ensures that forcibly killing a thread doesn't cause strange interference, such as leaving locks improperly released or classes half-loaded, which could confuse the JVM. The grace time costs CPU resources but ensures that the system behaves more predictably.

The grace period only consumes CPU time. After the abortion is triggered, the processor is considered "done" (with a result of Fail) from the strategy framework's perspective. The processor thread will continue running in the background, but the strategy framework will not wait for it. Instead, it will move on to the next processor(s) and begin their execution.

Refer to Understanding AProVE: Abortions and Timers for more infos on Timers and Abortions.