Thanks to a rich Petri net theory, there exists a broad range of veri cation techniques for Petri nets. Most of them have a performance that highly depends on the particular combination of net and property. That is why several veri cation tools for Petri nets use portfolio approaches where various veri cation algorithms are run concurrently. In this note, we sketch the architecture of a portfolio manager, using the tool LoLA 2.0 as a running example. The portfolio of a veri cation problem is organized as a task tree. The leafs of the task tree are actual veri cation algorithms while the inner nodes represent the logical structure of the portfolio. The portfolio manager schedules veri cation algorithms and assigns resources to them (processor cores, memory, and time). Moreover, it evaluates the consequences of returned results with regard to the original veri cation problem.
Karsten Wolf
There exist several approaches for veri cation, ranging from explicit model
checking [
The veri cation methods have in common that their performance on a
particular model is almost unpredictable. Most methods have an unpleasant
worstcase complexity ranging somewhere between NP-completeness and
EXPSPACEcompleteness [
That is why several contemporary tools such as Tapaal [
Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
In this paper, we shall discuss the architecture of a portfolio manager, the component of a Petri net veri cation tool that takes care of organizing a portfolio of veri cation algorithms. We use the portfolio manager of LoLA as a reference. However, we expect the central statements of the paper to be universal.
A portfolio manager has two main duties. First, it has to record the results of the launched veri cation algorithms and to trigger consequences for the remaining algorithms. Second, it has to schedule the resources (available processor cores and memory as well as available run time) to the running algorithms.
We shall rst discuss typical ingredients of a portfolio (Section 2). We then encapsulate veri cation algorithms in tasks, the main object to be treated by the portfolio manager (Section 3). Section 4 reveals the lifecycle of a task. Subsequently, we introduce task trees for representing the logical dependencies between the portfolio members (Section 5). Finally, we discuss the scheduling of tasks (Sections 6 and 7). 2
In this section, we give examples of veri cation algorithms that may serve as constituents of a veri cation portfolio.
Search algorithms Most veri cation problems can be solved by a traversal of the
state space or the product of the state space and an automaton representing
the veri cation problem. For reachability queries, a simple depth- rst traversal
of the state space is su cient. For model checking CTL formulas [
In all cases, search is subject to the state explosion problem. For concurrent
systems, the main application domain of Petri nets, stubborn set methods are
among the most important state space reduction methods. Stubborn set is a
whole family of approaches (see [
Consequently, a portfolio for reachability may already include two di erent search algorithms, one speculating on reachability of the predicate, the other speculating on unreachability of the predicate.
Similar pairs of stubborn set methods exist for other classes of properties as well.
Symbolic methods Symbolic methods include BDD based model checkers [
Petri net structure theory In [
Another purely structural approach is the invocation of the
siphon/trapproperty [
If a veri cation problem asks for the presence of just a few tokens on an initially empty place, it is unlikely that all of the 232 tokens of an initially marked place are needed. Therefore, a portfolio for reachability and selected other problems may include a special search routine where most tokens on places with a large initial marking are \frozen". We obtain an underapproximation of the original state space which means that the property is indeed reachable in the original state space if it is reachable in the underapproximation while it may or may not be reachable in the original state space if it is unreachable in the underapproximation.
The dual approach, overapproximations, do not make sense in explicit verication since they require more space that the actual state space. For symbolic model checking, however, overapproximations are a valid tool for reducing the size of BDDs. Skeleton net If the given net is a high-level net, we may consider the skeleton (the P/T net just obtained by ignoring colors). There is a net morphism between the high-level net and its skeleton, so some properties including reachability are preserved: if a marking is reachable in a high-level net, the corresponding marking is also reachable in the skeleton (the reverse is not true). Since it is very easy to obtain the skeleton from a high-level net, the approach may yield results for high-level nets that are too large to be unfolded to equivalent P/T nets. The MCC contains some high-level nets of this kind. For verifying the skeleton, we may again employ several algorithms such as search or the state equation.
If the original net is a P/T net, we may fold that into a high-level net for obtaining a skeleton, so the approach is applicable for both high-level and lowlevel input.
Strength reduction For some property , there may be a simpler property that implies or is implied by . Adding a veri cation algorithm for the simpler property may thus help for verifying . For instance, satisfaction of the CTL property EF is necessary for satisfaction of E( U ) while AG is su cient for EG . The pure reachability problems EF and AG are indeed simpler since they enable the use of additional veri cation algorithms such as the state equation approach mentioned above.
Random walks For properties where the witness or counterexample is just a single nite path, one can simply launch random walks through the state space. If such a walk hits a witness (counterexample), the property holds (does not holds) while otherwise the method does not terminate. The method is extremely memory-e cient since we do not need to store visited states. At the same time, it can re transitions at an extremely high rate as we do not need to search nor store markings. Consequently, random walks are a poor veri cation method when applied standalone, but a very useful member of a portfolio. The likelihood of hitting a witness or counterexample path can be increased by applying suitable stubborn set methods in the selection of the next transition to be red. Boolean combinations If a formula to be veri ed is a Boolean combination, subformulas can be veri ed separately. That is, the veri cation algorithms for the individual sub-formulas establish separate portfolio members.
Conclusion Portfolios may be large (with more than 10 constituents) and diverse. We have complete and incomplete methods (incomplete in the sense that they do not always terminate, or may terminate without a de nite answer to the problem). Methods may answer to the original problem or only to a sub-problem. Methods have a broad range of expected memory and runtime consumption. It is therefore necessary to establish a structured approach to portfolios, the portfolio manager.
With the concept of a task, we design an object that encapsulates a particular veri cation algorithm and augments it with all necessary information to execute it as a portfolio member. These data include the necessary inputs, the status of the task in its lifecycle (see Section 4), results and statistics (for completed tasks), assigned resources (discussed in Section 7), and data that are relevant for execution and scheduling (also discussed there).
Input Currently, LoLA is called with a single Petri net and a list of veri cation
problems, given as CTL* formulas. This standard is established by the setup of
the MCC. However, a veri cation tool needs to internally deal with more than
one net and more than one formula, independent of the original input. Multiple
formulas come into play since we may want to separately verify sub-formulas
if the veri cation problem is a disjunction or conjunction. In addition, we may
add distinct formulas using the strength reduction explained in Section 2. If we
apply the skeleton approach explained in the same section, we have two distinct
nets for every given veri cation problem. In addition, we may want to apply
net reduction [
Beyond the plain yes/no answer to the veri cation problem approached by a task, results may include additional diagnostic information such as witness or counterexample paths as well as witness or counterexample states. If search algorithms use storage methods based on Bloom ltering, diagnostic information may include a likelihood of hash con icts that may be used for judging about the risk that the state space is actually incomplete.
Statistical information includes the number of visited states, red transitions, run time, consumed memory and other information that is useful for evaluating the performance of the algorithm or the di culty of the problem instance with respect to the veri cation algorithm. 4
IDLE This is the initial state of the lifecycle. The task is created as a result of the
planning phase of the veri cation tool. The planning phase of a veri cation tool
is run subsequent to parsing the net(s) and veri cation problem(s). For temporal
logic formulas, rewriting is applied [
ACTIVE An active task is ready for execution, This means that all preprocessing of inputs is completed. The task is just lacking the assignment of resources for execution by the scheduler that is part of the portfolio manager. RUNNING A running task is executing the actual veri cation algorithm. During this phase, there are two kinds of interaction between the algorithm and the portfolio manager. First, the portfolio manager controls the use of resources assigned to the task. We discuss this issue in Section 6. Second, the portfolio manager collects status data of the algorithm (e.g. number of markings visited so far, number of red transitions, etc.). Such status information is quite useful to give the user the impression that the tool is running properly. The status information needs to be aggregated for all running tasks in order to create a readable display.
Figure 2 shows an example of an aggregated status report in LoLA. The rst block reports all veri cation problems (referred to by an identi er) which have already been solved, their category, their value, and the portfolio member that delivered the result for that particular problem. The second block displays, for every other formula, the number of portfolio members that are available for that problem, and the status of these tasks. The third block displays the running tasks with the type of underlying algorithm (in the example: three times state equation and one depth- rst search), their assigned resources, and the algorithmdependent status information collected by the portfolio manager. FINISHED A nished task has completed the execution of its veri cation algorithm and delivered its result.
OBSOLETE A task is obsolete if its result is not needed anymore to determine the answer to an original veri cation problem. If, for instance, a veri cation problem is a disjunction of two subproblems, and one of the subproblems is found to be true, all tasks supporting the other subproblem become obsolete. The main factual di erence between a nished and an obsolete task is that statistical information and results such as counterexamples or witnesses are present and meaningful only for nished, but not for obsolete tasks.
CANCELED/T, CANCELED/M Tasks are canceled as soon as they exceed their assigned resources. We distinguish cancelation by exceeding the time limit from cancelation by exceeding the memory limit. This way, we may consider rescheduling the task if, later on, additional resources become available. SUSPENDED A task is suspended if assigned resources are not available. Consider, for example, memory resources. A task, for instance a search algorithm, does not need all its memory resources immediately. So we may optimistically assign more memory resources than actually available at a certain point in time, speculating that another task will meanwhile release its resources. Suspending a task permits a seamless continuation of an already running task as soon as required resources are indeed available. The di erence between a suspended task and a canceled task is that a canceled task releases all assigned resources while a suspended task keeps its resources and may resume execution. Resuming a canceled task amounts to re-execution from the beginning. 4.2
preprocess (IDLE to ACTIVE) This transition is triggered by the completion of the preprocessing routines for the inputs to the task. In the LoLA implementation, we use the pthread condition mechanism to announce the completion of preprocessing routines.
The amount of necessary preprocessing depends on the veri cation algorithm. While search algorithms require intensive preprocessing (as already explained), the state equation approach just needs a simple net structure for deriving the incidence matrix. When skeleton nets are involved, we may skip net reduction since the resulting nets are already quite small. An individual transition from idle to active permits an early start of the actual veri cation. We may run tasks that require little preprocessing while other tasks are still in the preprocessing phase. If such early tasks deliver their result quickly, we may be able to skip some of the preprocessing thus saving resources for other veri cation problems. launch (ACTIVE to RUNNING) We launch a task by spawning a new thread for the actual veri cation algorithm of the task. The transition is triggered by the scheduler which is discussed in Section 7. report (RUNNING to FINISHED) When a veri cation algorithm terminates, it triggers the report activity. The results of the algorithm (value, witnesses or counterexamples, statistics) are recorded in the portfolio manager. Resources assigned to the task are released and a signal is sent to the portfolio manager that triggers the next scheduling activity (for launching another task). timeout (RUNNING to CANCELED/T), memory exhausted (RUNNING to CANCELED/M) These activities are triggered by the resource management of the portfolio manager. We discuss this issue separately in Section 6. suspend (RUNNING to SUSPENDED) This activity is triggered by the resource management of the portfolio manager. Suspension happens if a task is acquiring a granted resource tat is not immediately available. The thread executing the veri cation algorithm is frozen until the request can be satis ed. resume (SUSPENDED to RUNNING) When some task releases its resources (through cancelation or termination), the resource manager may trigger the resume transition and grant fresh resources to a suspended task. reschedule (CANCELED/T to RUNNING) The actual runtime of a veri cation algorithm is virtually unpredictable. It may this happen that a task needs much less runtime than originally scheduled. This way, additional runtime may become available. If, after having executed all tasks once, more runtime is available than originally scheduled for some canceled task, we may reschedule that task. Giving more runtime to it, we gain some opportunity to nish it successfully this time. obsolesce (any to OBSOLETE) A task becomes obsolete if some other task for the same veri cation problem has answered the given problem. As soon as any task executes its report transition, all other tasks for the same veri cation problem are checked whether they can still contribute to the original problem. If not, they become obsolete. In case they are currently running or suspended, execution is stopped and resources are released. Obsolete tasks are detected by the evaluation of task trees to be introduced in Section 5.
Conclusion Tasks have a complex life cycle. The transitions of the lifecycle are triggered by various components of the veri cation tool. Consequently, portfolio management requires a clean assignment of responsibilities to the various components. We have been experimenting with the portfolio manager of LoLA for several months before the structure of the lifecycle converged to the one just reported. 5
The leafs of the task tree are the tasks as discussed so far. Whenever tasks complete, the result value is propagated bottom-up in the tree. Whenever an inner node gets a nal truth value, the remaining branches The inner nodes re ect the logical dependencies between the portfolio members. We identi ed several useful types of inner nodes and discuss them one by one. Conjunction This binary (or n-ary) node re ects the fact that the original problem is a conjunction of subproblems. The children of a conjunction node are the roots of the portfolios of the subproblems. The following table re ects the propagation of values of a conjunction node.
true false unknown void true true false unknown void false false false false false unknown unknown false unknown void void void false void void Disjunction This binary (or n-ary) node re ects the fact that the original problem is a disjunction of subproblems. The following table re ects the propagation of values.
true false unknown void true true true true true false true false unknown void unknown true unknown unknown void
void true void void void Aggregation This binary (or n-ary) node represents a portfolio where two (or more) algorithms are available for exactly the same (sub-)problem. It propagation behavior can be re ected in the following table.
true false unknown void true true (error) true true false (error) false false false unknown true false unknown void
void true false void void
There are two entries marked with error. If any of these situations would ever occur, one of the involved veri cation algorithms is wrong, or has an incorrect implementation.
Dual This is a unary node in the task tree. It maps a veri cation problem to the corresponding dual problem. Using the dual node, we may have algorithms for reachability in a portfolio of an invariance problem, to name just one example. Whenever a dual node occurs, the veri cation problem of the child node refers to the negation of the veri cation problem for the current node. In the mentioned example, if we want to verify AG , the child node is attached to formula EF : . The behavior of this node is de ned by the following table.
true false unknown void false true unknown void Su cient This unary node is used if the result of the child node only establishes a su cient condition for the original veri cation problem. If, for instance, the original problem is EG , a portfolio for AG can be wrapped with this node to re ect that, if the answer to AG is false, this does not means that EG is false, while a true answer to AG means that EG is indeed true. The following table can be used.
true false unknown void true unknown unknown void Necessary This unary node is the dual counterpart of a Su cient node for necessary conditions (such as EF for E( U )). Its table looks as follows.
true false unknown void unknown false unknown void
The original problem is the CTL formula EF ^ AG EF , for any state predicates and . This original problem forms the root of the task tree. The conjunction node signals that the two sub-formulas are veri ed separately. The rst sub-formula, the reachability problem EF , can be approached using the original net or the corresponding skeleton net (obtained by folding if N is a P/T net). These alternatives are modeled as an aggregate node. Reachability in the skeleton is only a necessary condition for reachability in the original net, so the results of the left branch are ltered by a necessary node. This way, despite possible true and false answers of the underlying algorithms, only a false result is propagated towards the root. The aggregate node below the necessary node re ects the fact that reachability in the skeleton can be investigated by two algorithms: evaluation of the state equation or depth- rst search. For the original net, the task tree o ers three alternative approaches: state equation, depth- rst search, and an underapproximation that tries to freeze tokens in the initial marking. Reachability in the underapproximation is a su cient condition for actual reachability. However, we do not need a su cient node here since the algorithm itself would only answer yes or unknown.
For the sub-formula AGEF , the task tree o ers three alternative approaches. The one displayed in the middle is conventional depth- rst search that, through investigation of strongly connected components, is able to answer the task. This search is anked by a su cient and a necessary condition that both have been obtained by strength reduction. Indeed, a net satisfying AG also satis es AG EF , and a net satisfying AG EF must also satisfy EF . The verication of AG is traced back to the veri cation EF : using the tautology AG () :EF : . This way, actual veri cation algorithms only need to care about reachability and not about invariance. The dual node in the task tree is responsible for negating the result of the underlying algorithm. For checking the necessary criterion EF , we employ the state equation and depth- rst search in the skeleton.
The example shows the potential complexity of a portfolio and demonstrates the necessity of a systematic approach. 6
Cores, memory, and runtime are the critical resources when running a portfolio. If the number of algorithms executed in parallel exceeds the number of available cores, the operating system is forced into frequent context switches, with negative impact on overall runtime and on caches. Since depth- rst search is extremely space-consuming, we have to take care that algorithms running in parallel have a well-designed way of competing for memory. Last but not least, we need to make sure that all portfolio members get a fair portion of available runtime, if that is limited. The actual scheduling of resources is discussed in the next section. We can schedule resources only if we can control the access of tasks to these resources. That is why we included this section.
For controlling access to cores, we believe that it is su cient to take care that we launch at most as many parallel threads (i.e. concurrent veri cation algorithms) as there are cores in the underlying machine. In case of LoLA, the user speci es that number using a command-line option. Runtime is controlled by an additional timer thread that is running as long as the portfolio manager is active. It is executing an in nite loop where, after sleeping for ve seconds, it checks for tasks that have exceeded their time limit and, at the same time, collects status information from running tasks and displays them. According to our experience, the granularity of ve seconds seems to be su cient for controlling time limits of tasks. By sleeping a long time between activities, the timer thread does not severely interfere with the threads that execute the actual veri cation algorithms.
The most interesting resource with respect to resource control is memory. As a preliminary step, we discuss access to memory in general. Based on this discussion, we can then propose a strategy for controlling the amount of memory assigned to a task.
Depth rst search, the main method for explicit veri cation, is an extremely memory-consuming task. Pro ling with LoLA revealed that, during depth- rst search, about 90% of the runtime is spent for checking whether or not the currently visited marking has been visited before, and to insert it into the data structure if it has not visited yet. To our own surprise, about 40% of that time is spent in malloc, the C routine for allocating memory on the heap of the main memory (including calls to the corresponding new operator in C++). The explanation of that large percentage has two aspects. First, it shows that the remaining parts of a depth- rst search algorithm indeed have an extremely lightweight implementation. Second, it shows that allocating memory on the heap is a rather involved task. First, malloc needs to nd a suitable portion of memory in the list of free memory segments, and to launch a call to the operating system if there is none. Second, it needs to take precautions for the eventual return of the memory to be allocated. And nally, malloc must be thread-safe, i.e. it must provide a mechanism for mutual exclusion between concurrent calls to the routine.
Based on this analysis, we conclude that depth- rst search should include a tailored memory management. In LoLA, we allocate memory in large pages of, say, 100 Megabytes. Then, our own memory manager allocates portions of such a page to individual requests of the search algorithm. We obtain the following runtime bene ts: { Since every concurrent depth rst search uses its own memory management, we do not need to provide any mechanism for mutual exclusion during memory management; { Since memory allocated for depth- rst search is never returned before that search as such is nished, we do not need to provide any mechanism for returning memory to the list of free portions; { Since memory is never returned, we have no fragmentation issues and memory management is mostly trivial; { When depth- rst search terminates, or is canceled, we only need to return the allocated pages instead of freeing hundreds of millions of individual data objects.
The rst three items cause a speedup of 20% for our own memory allocation requests, compared to traditional calls to malloc. The last item reduces the time for terminating a depth- rst search from several minutes to a fraction of a second. Hence, the page mechanism is a prerequisite for running nontrivial portfolios.
Once we have a page based memory management for depth- rst search, we can gain complete control of the memory usage. We simply need to count (and limit) the number of pages that the memory manager of a depth- rst search is allowed to allocate. A task is suspended by simply not answering to its request for memory. A task can be canceled by not answering to its memory request while releasing its resources (otherwise, canceling a pthread is a nontrivial endeavor).
Other veri cation algorithms involve depth- rst search as well, like our underapproximation approach, or require only marginal memory resources, like random walks. For two classes of algorithms, we do not provide any control of their memory usage in LoLA: state equation and siphon/trap property. Here, we use o -the-shelf libraries for solving linear problems resp. SAT problems and so far we did not dare to intervene in their memory management. However, both problems are in NP and thus in PSPACE, so we hope that their memory requirements are less severe than that of depth- rst search. With this sloppy way of controlling memory resources, we at least managed to stay within the harsh memory limit of 16 Gigabytes in recent issues of the MCC. 7
Scheduling refers to two kinds of decisions to be repeatedly taken in a running portfolio manager. First, we need to select the order in which we execute tasks. Second, we need to decide how many resources we assign to the selected tasks. As long as we do not have a strict limit for runtime, the order of executing tasks is less important. That is why we discuss this issue under the assumption that there is in fact a time limit. Using such a strategy in a scenario without time limit, helps us to reduce the overall run time in many cases but has no severe impact if it fails.
So, assuming a strict time limit, our duty is to get as many as possible rm
results (true or false) for the given veri cation problems. In [
Concerning the net, large nets tend to be more challenging than small nets. Nets with large con ict clusters tend to be more challenging than nets with small con ict clusters (more concurrency means better applicability of stubborn sets).
Regarding a temporal logic formula, the number of occurring temporal
operators seems to be a good basis for judging its di culty. The simplest case
are without doubt formulas without temporal operators. They correspond to
constants true or false, or to a state predicate that can be evaluated by just
inspecting the initial marking. Such formulas frequently appear in the MCC as
the result of linear programming approaches to the atomic propositions and
application of temporal logic tautologies [
Of the remaining formulas, the ones with one or two temporal operators are
the simplest. Most of these formulas are supported by specialized algorithms
[
Formulas with more than two temporal operators occur less frequently in
practice. That is why the number of occurring operators appears to be a su
cient criterion for judging their complexity. Alternatively, LTL formulas could be
judged according to the number of states of the Buchi automata that represent
the formulas and which are used in LTL model checking [
For formulas with the same temporal structure, the number of places mentioned in the formula is another criterion for di erentiating the di culty. A large number of mentioned places leads to a large number of visible transitions.
The overall di culty of a problem would be some Pareto style aggregation of the di culty of the formula and the di culty of the net. In LoLA, we currently consider only the di culty of the formula.
For search algorithms, we schedule the easiest problems rst. If any of the problems is solvable then the easiest ones have the greatest likelihood to do so. For algorithms that require only few resources, such as random walks, we schedule the most di cult problems rst. If a problem is indeed di cult, it appears to be easier to land a lucky punch with an unusual algorithm than with a state space exploration. In any case, we schedule tasks in a way that, if possible, tasks running in parallel concern di erent problems. In the case where some problems indeed turn out to be simple, we solve them without running too many algorithms in parallel on them, so more time remains for the challenging problems. 7.2
Cores For sequential algorithms, a single core is assigned. This is the case for the whole LoLA portfolio manager. For parallel algorithms, it could be reasonable to assign more than one core. Here we have a con ict between assigning cores to that algorithm versus assigning cores to other portfolio members. To date, most parallel algorithms have a saturating behavior with respect to the number of cores. That is, there is a number of cores where additional cores do not lead to an improvement of runtime. If that number is known (by experimental evidence), it would be reasonable to assign not more than that number of cores to the parallel algorithm, and cores might be left for other portfolio members.
Memory The memory-critical tasks are those that execute depth- rst search. We pointed out above that, depending on the stubborn sets used, they are optimized for true (e.g. reachable) or false (e.g. unreachable) cases. One of the cases (reachable) bene ts from the on-the- y e ect while in the other case the whole reduced state space needs to be computed. For memory assignment, we may derive two conclusions. First, if the task is set up for the case where we bene t from the on-the- y e ect, the task either delivers its result after having consumed only few memory pages, or it is unlikely to deliver a result at all. Second, if the task is setup for the case where the whole reduced state space needs to be computed, we either assign su cient resources for nishing the search, or any assigned resource is wasted. In consequence, taking reachability as an example, we assign only few pages for tasks where search is optimized for reachability and we assign a lot of memory to tasks that are designed for unreachability. In the portfolio manager, we distinguish search (optimized for reachability) from exclusive memory (optimized for unreachability) tasks. The scheduler takes care that, at all times, only one exclusive memory task is running. All the other tasks get a xed small number of memory pages assigned, and the single exclusive memory task basically is permitted to use all remaining memory. Runtime For runtime, we identi ed two major scenarios: limited versus unlimited availability. For the use of veri cation in practice, we expect that an unlimited amount of runtime is available. For search tasks, the monotonic request for memory establishes some bound for runtime anyway. For constant-memory tasks such as random walks, a scenario with unlimited runtime should implement some criterion for interrupting the method (number of tries or an algorithm-speci c local time limit). Otherwise, we can schedule tasks as soon as cores and memory are available.
Use cases with a strict time limit include the MCC conditions as well as practical situations where we have a rm deadline for reporting results. Taking into consideration that we can schedule at most one exclusive memory task at a time, we propose the following strategy. First we separately schedule all remaining exclusive memory tasks. We compute the available time as the di erence of deadline and current time. If an exclusive memory task is currently running, we replace the current time with the start time of the running task. This amount of time is divided by the number of remaining (and running) exclusive memory tasks. Every task is given that amount of time. The end time of the running task is replaced accordingly.
For all other tasks, we can use all available cores if no exclusive memory task is present, and we can use all but one core if there are remaining exclusive memory tasks. Depending on that number of tasks, we compute the largest number n of seconds such that all nonexclusive tasks can be scheduled for n seconds before the deadline expires. This is a bit tricky since we need to take care about already running tasks, and we need to re ect the fact that the runtime for a single algorithm cannot be parallelized. That is why the calculation requires more e orts than just dividing the available time by the number of remaining tasks.
We compute the remaining time per core which is the di erence between the deadline and the start time of an already running task (there should be as many such tasks as we have available cores). If less tasks are running, we use the current time instead. Let k be the number of available cores, and n be the number of remaining nonexclusive tasks. Then we schedule n div k tasks for every core. The remaining n mod k tasks are schedule for the cores with largest remaining time. Then we can compute, for every core, the remaining time on that core and distribute it equally for the tasks planned for this core. That is, tasks do not necessarily get exactly the same time, but processing resources are used exhaustively.
We repeat the scheduling procedure every time a new task is checked in, or a running task nishes. This way, we continuously adapt our scheduling to the current situation.
Example. Suppose that we have four cores, and initially two exclusive memory tasks and ten other tasks. Let 1000 seconds be available. Then we would launch one exclusive memory task with a time limit of 500 seconds. For the remaining cores, we would assume a distribution of four versus three versus three tasks, so we would launch one task with 250 seconds, and two tasks with 333 seconds time limit. If, after 100 seconds, a non-exclusive task returns a result, we have nine remaining tasks (including the running tasks). Two cores have an available runtime of 1000 seconds (since the two running tasks have been launched initially) and the third core has 900 seconds remaining time. We have a distribution three versus three versus three, so we would launch a new task with a time limit of 300 seconds. If, after 200 seconds (counted from beginning), the exclusive memory task returns, we launch the remaining exclusive memory task with a time limit of 800 seconds. If it returns after 250 seconds (again counted from beginning) an additional core becomes available for the non-exclusive tasks. The individual available time is 1000 versus 1000 versus 900 versus 750 seconds and there are nine remaining tasks. So we would distribute them by the pattern three versus two versus two versus two. In e ect, one of the running tasks would keep its time limit of 333 (= 1000 / 3) seconds. The second task that was started in the very beginning would get a new time limit of 500 (= 1000 / 2) seconds. The task started after 100 seconds would get a new time limit of 450 (= 900 / 2) seconds, and we would launch a fresh task with a time limit of 375 (= 750 / 2) seconds.
Using this scheduling policy, we bene t from low hanging fruits earned early in the scheduling sequence. If tasks nish early, remaining tasks immediately get more run-time assigned.
Sometimes it may happen that remaining tasks do not exhaust the scheduled time. In this case we check whether we have tasks that were canceled before due to lack of time. If they consumed less time than still available in the end, we reschedule such a task with a more generous time limit. 8
We have discussed the main design decisions to be made for the implementation of a portfolio manager for Petri net based veri cation. Due to the size and diversity of veri cation portfolios, a systematic approach is necessary. We also discussed possible deviations from the decision that we made in the LoLA tool. Since the rst implementation of the task manager, we added several new veri cation algorithms to the portfolio and found that the design of the portfolio manager was robust with respect to the changes. This way, the integration of the new methods validated our major design decisions.
Our next step for improving the manager will be a prognostic feature for memory consumption. We observed that search algorithms request new memory at a roughly constant rate. We can use the past rate of memory requests for estimating the future memory requirement of an exclusive memory task. This way, we may be able to assign additional memory to nonexclusive tasks.