George Bosilca

Aurelien Bouteiller

Thomas Herault

Valentin Le Fèvre

Yves Robert

Jack Dongarra

Distributed Termination Detection for HPC Task-Based Environments

Keywords: Termination Detection, Credit Distribution, Task-based Runtimes, MPI Détection de terminaison, Distribution de crédit, Systèmes de tâches, MPI

This paper revisits distributed termination detection algorithms in the context of high-performance computing applications in task systems. We first outline the need to efficiently detect termination in workflows for which the total number of tasks is data dependent and therefore not known statically but only revealed dynamically during execution. We introduce an efficient variant of the Credit Distribution Algorithm (CDA) and compare it to the original algorithm (HCDA) as well as to its two primary competitors: the Four Counters algorithm (4C) and the Efficient Delay-Optimal Distributed algorithm (EDOD). On the theoretical side, we analyze the behavior of each algorithm for some simplified task-based kernels and show the superiority of CDA in terms of the number of control messages. On the practical side, we provide a highly tuned implementation of each termination detection algorithm within PaRSEC and compare their performance for a variety of benchmarks, extracted from scientific applications that exhibit dynamic behaviors.

Introduction

A distributed application is terminated if all processes have completed the computations assigned to them and no message is in transit within the interconnection network. Termination detection is a fundamental issue for distributed systems, because -for dynamic applications -no process has complete knowledge of the global configuration (the state of all processes and of the network) [START_REF] Fokkink | Distributed Algorithms: An Intuitive Approach[END_REF]. In particular, an idle process may be reactivated by a message from another process, complete its new assignment, send some work orders to be completed by remote processes, and then become idle again and so on. Many active-to-idle and idle-to-active transitions can take place before the application eventually terminates. Since the pioneering work of Dijkstra, Scholten, and Francez [START_REF] Edsger | Termination Detection for Diffusing Computations[END_REF][START_REF] Francez | On achieving distributed termination[END_REF], countless algorithms have been proposed for termination detection.

Many high-performance computing (HPC) applications can rely on straightforward techniques for termination detection. For instance, many dense or sparse factorization algorithms terminate when the bottom-right diagonal element of the matrix has been updated, and termination can safely be declared right after the completion of that last operation. More generally, many HPC applications are structured as a task graph with all dependencies statically known before execution. Termination can safely be declared once all exit tasks (tasks without any successor task) of the graph have been completed. However, there are also many HPC applications the task graphs of which are dynamically updated during the execution: the application task graph is data dependent, and new tasks may be created depending on the value of the output of another task. Typical examples are partial differential equation (PDE) schemes, where the necessary degree of refinement is dictated by the physics of the simulated material. For all of these applications, a distributed termination detection algorithm must be implemented. Our main contribution is to provide a new termination detection algorithm that is specialized for HPC platforms and considers the particular challenges inherent to their scale and interconnect properties. For instance, HPC application workloads are often communication intensive and latency/injection rate sensitive, with detrimental implications for algorithms that delay, or add extensive management of, application messages. In this paper, we consider different classes of termination detection algorithms and evaluate their behavior with respect to this HPC-centric machine and workload context.

We distinguish and compare three main classes of algorithms for termination detection. First, many algorithms use ascending and descending waves of control messages, and we discuss the Four Counter algorithm (4C) -a state-of-the-art wave algorithm -in Section 3. The Credit Distribution Algorithms (CDA) are another set of algorithms proposed independently by Huang [START_REF] Huang | Detecting termination of distributed computations by external agents[END_REF] and Mattern [START_REF] Mattern | Global quiescence detection based on credit distribution and recovery[END_REF]. These algorithms are also known as weight-throwing algorithms, and they use a controlling agent that ini-tially distributes some credit to all processes. When sending an application message, a process keeps a fraction of its current credit and transfers the remaining fraction through the message; upon reception of a message, the credit carried by the message is added to the credit of the receiving process. Finally, when becoming idle, a process returns its credit to the controlling agent. The controlling agent declares termination when all of the initially distributed credit has been returned to it. We introduce the original algorithm, "Huang's CDA" (HCDA), discuss several existing variants, and propose a novel CDA algorithm dedicated to HPC platforms in Section 3. Finally, a more recent class of algorithms, Efficient Delay-Optimal Distributed (EDOD) termination detection algorithms [START_REF] Nihar | An efficient delay-optimal distributed termination detection algorithm[END_REF], requires that a control message acknowledging primary messages reception is sent by the receiver of each application message back to the sender; this is to ensure that the sender can be safely declared terminated once all of its messages have been acknowledged. These control messages go up and down a control binary tree -independent of the application communications. EDOD is carefully designed to minimize the latency of termination detection, and we describe it in more detail in Section 3.

Our main contribution is the design and implementation of a novel CDA variant that drastically improves performance, under the constraints of an HPC system, with a more conservative but mathematically accurate credit management system, where the borrowing operation can be satisfied by a neighbor process with more abundant resources. We evaluate the algorithms through [START_REF] Stephen | Starting with termination: A methodology for building distributed garbage collection algorithms[END_REF] a theoretical analysis in terms of control messages for two applications, the token ring, and synchronous tree-based task systems; and through [START_REF] Bosilca | PaRSEC: Exploiting Heterogeneity to Enhance Scalability[END_REF] extensive experiments conducted in a task runtime system. We provide an optimized implementation for the four algorithms under study and avoid non-scalable messaging patterns with hotspots at processes with a large number of neighbors. This will allow us to focus on the number of messages generated by each algorithm as the key indicator of performance and overhead.

The paper is organized as follows. In Section 2, we present motivating applications and systems that require termination detection. We review 4C, HCDA, and EDOD in Section 3. We introduce our new CDA algorithm in Section 4 and provide a theoretical comparison with 4C and EDOD in Section 5. We report extensive experiments in Section 6, showing that CDA dramatically outperforms HCDA and has a much smaller impact on execution for real-world applications than both competitors (4C and EDOD). Finally, in Section 7 we survey related work. We provide concluding remarks and directions of future work in Section 8.

2 Dynamic Applications, Task-Based Runtime Systems, and Termination Detection

Termination detection is often implicit or trivial in regular, static applications, for which the control-flow of the application and/or the initial load balance of the work is sufficient to decide, locally, the termination. The issue becomes more crucial for dynamic applications expressed over asynchronous programming paradigms, for which the total amount of work is data dependent-and therefore remains unknown until completion. Here, we focus on efficiently detecting that an application producing supplementary work and messages, from process-local criterion, is globally complete.

To illustrate the concept, we introduce an example: k-dimensional trees that represent approximations of multidimensional functions and operators. Consider for k = 1 a function, f (x), that should be approximated over a domain, [A, B]. A 1-D tree is used to approximate the values of f by splitting [A, B] into subdomains, [a i , b i ). For each subdomain, a leaf in the tree is created that carries a single value: the average of f in that subdomain, b a f (x)dx/(b -a). The size of the subdomain (and thus the quality of the approximation) is set by selecting the depth of the leaves in the tree. Figure 1 illustrates this approach. A task-based approach to create such representations is used in the Multiresolution ADaptive Numerical Environment for Scientific Simulation (MADNESS) [START_REF] Harrison | MADNESS: A multiresolution, adaptive numerical environment for scientific simulation[END_REF], which is a high-level software environment for the resolution of integral and differential equations in multiple dimensions using adaptive and fast harmonic analysis methods with guaranteed precision. The operation of creating a tree that represents a given function in a given domain for a target precision is called a "projection." A natural and efficient algorithm to implement the projection consists of walking down the tree in parallel, with each task instantiating a node and deciding locally if a given node in the tree is refined enough to reach the target precision, in which case it is defined as a leaf. If not, its 2k children are spawned to increase the refinement. As the algorithm proceeds with refining the nodes, a mapping defines which tasks/nodes are held by which process of the par-allel application. Depending on the targeted function, refinement, and data distribution, a process may be done with all current tasks but still receive more tasks to instantiate higher refinements at any time-until all processes are finished with all tasks.

A naive approach to detect termination would be to: every time a task spawns refinement nodes, wait for the entire subtree to complete before letting the task complete. This approach has multiple obvious drawbacks: if the wait monopolizes computing resources, a starvation will occur when the number of nodes in the k-dimensional tree exceeds the number of computing elements. Even if better strategies are implemented to avoid this resource consumption, control information about the completion of each task must be sent to the process holding the parent node, thereby introducing large delays and costs. Because a process may receive work at any time, local observations that the number of tasks to complete has reached zero is not sufficient to decide termination, and a distributed termination algorithm is necessary.

This issue occurs in many tree-based algorithms and is a key part of composition. Occurring frequently in MADNESS algorithms, multiple functions must be projected in order to be derived, summed, multiplied and integrated to compute a solution to the final problem. To reduce overhead, all of these operations should start with maximum concurrency, but knowledge about the completion of dependent operations is necessary to ensure the correctness of the result. Distributed termination detection algorithms rely on observing the activity of the processes, as well as the injection and delivery of application messages, sometimes modifying them to piggyback information. Since these roles are assigned to the runtime system, it is also natural to assign the role of detecting the termination of global operations to the runtime environment.

Algorithms for Termination Detection

Sections 3.2 to 3.4 detail the main features of the three primary detection termination algorithms from the literature: 4C (waves with in-transit message detection), EDOD (acknowledged primary messages), and HCDA (Huang's credit distribution), which we contrast with our own CDA algorithm in Section 4. Beforehand, in Section 3.1, we review the system model common to all algorithms.

System Model

We consider a distributed system comprised of a set of P processes with an independent clock and a local memory. The processes are connected through an asynchronous interconnection network capable of carrying messages in 1-port duplex mode with an arbitrary, but finite, delay. Processes and messages are considered here in the general sense: processes may employ internal shared-memory parallelism (which is abstracted from the model), and remote memory accesses can be considered as asynchronous messages. The processes and network are reliable, and we assume that the interconnection network is complete; that is to say: any process may send a direct message to any other processes. We also assume that messages may not overtake; in other words, the network is assumed to be FIFO, or the network library manages ordering and reemission as necessary (e.g. MPI). Although not required for correcting the algorithms, these assumptions simplify performance analysis.

A parallel workload executes internal actions on the processes, either executing a task or creating a new task. Task mapping (to processes) is determined by an application-provided mapping function, and successor tasks may be mapped onto a remote process, which entails the emission of a message. When the destination of a message is the local process, it is considered a local action.

In such a distributed system, we consider the termination detection problem. Termination detection is achieved when all processes know that every process has completed the workload. More formally, a process is still considered active when it has pending actions, including when it is executing a task, has scheduled tasks to execute locally, or has pending emissions to perform. When a process does not have any further pending local actions, it becomes idle. A process may exit from the idle state and return to the active state only when it receives a message (i.e., tasks can be only created upon completion of another task). Without loss of generality, we consider that, initially, one process contains a startup task (there is a trivial transformation to render any workload with multiple initial tasks compliant). The termination of the workload is a global stable state that is reached when, in a global snapshot [START_REF] Chandy | Distributed Snapshots: Determining Global States of Distributed Systems[END_REF], every process is in the idle local state, and there are no in-transit messages (since, otherwise, these in-transit messages would create work for some of the idle processes). The termination is detected when every process has been informed that this global state has been reached.

Termination detection algorithms are thus distributed algorithms that observe that the global state has been reached and then announce it to all processes. In some algorithms, the detection and announce phases may be merged or overlapped. The distributed termination detection algorithm likely requires the exchange of secondary messages (i.e., supplementary control messages added to the primary messages generated by the parallel workload). These secondary messages allow the process states to be gathered/reported to a centralized entity or be part of a termination broadcast.

The 4C Wave Algorithm

In wave algorithms, when a process becomes idle, it initiates a wave to verify the state of other processes in the system. The wave crosses the network and collects the status of individual processes and their communication channels at some process -either at the initiator or at some external entity. That process then inspects the collected global state to ascertain when the global termination state has been reached. For example, a process that switches from active to idle may initiate a distributed snapshot. The snapshot permits to detect in-transit messages, i.e., messages that have been emitted before the beginning of the wave, but received after its beginning at another process. Thus, after completing the snapshot, a process can report to the announcer if it was active, or if it detected an in-transit message at the logical time of the snapshot. Unfortunately, this approach requires performing a large number of waves. Specifically, one wave for every process's transition from active to idle, which -in the worst case -may result in as many waves as primary messages. The approach also suffers from a large termination detection delay.

The 4C wave algorithm, which has seen some practical uses [START_REF] Harrison | MADNESS: A multiresolution, adaptive numerical environment for scientific simulation[END_REF], can avoid some of these caveats. In this algorithm, processes are organized along a secondary tree overlay, and the root of that tree announces when termination is detected. Every process, p, counts how many primary messages it has sent, s p , and received, r p . It also maintains two accumulating counters, σs i p and σr i p , initially set to 0, representing the cumulative number of primary messages sent and received by all processes in the subtree rooted at p -as collected during wave i.

Independent of their idle or active state, processes can be in the UP or DOWN state (UP initially). When a leaf in the tree becomes idle in the UP state, it enters the DOWN state and sends its two counters to its parent in a STOP message. When a node in the tree receives a STOP message from its children, it accumulates the counters. When it becomes idle in the UP state and has received a STOP message from all of its children, it enters the DOWN state and propagates the counters to its parent.

When the root enters the DOWN state, it compares σs i root , σr i root , σr i-1 root , and σs i-1 root . If they are all equal, it broadcasts the termination; otherwise, it sends down a REPEAT message (propagated by all) that initiates the nodes' transition from the DOWN state to the UP state (thus starting another wave).

Comparing σs i root and σr i root is not a sufficient condition for termination, as one has to account for orphan messages, i.e., messages emitted by some process after the wave and received by some other process before the wave. If the wave is crossed by orphan messages, the reception is counted in the accumulator, σr i root , but its emission is not. Thus, an orphan message may cancel the difference, σr i root -σs i root , even when an in-transit message is present, which would render the algorithm incorrect. If the value of σs i root remains constant during two consecutive waves, then the prior wave had no orphan messages, hence the counter comparison is a valid estimator for the absence of in-transit messages.

Optimal Delay Algorithm

Mahapatra and Dutt [START_REF] Nihar | An efficient delay-optimal distributed termination detection algorithm[END_REF] note that many termination detection algorithms focus on optimizing for the minimal number of secondary messages but often exhibit poor detection delay on commonly used primary communication patterns, like k-ary n-cubes, especially when considering a bounded port model, where message management time is considered. For this reason, the authors focus on designing an algorithm the purpose of which is to attain the optimal detection delay on arbitrary primary communication patterns. Their EDOD algorithm requires that primary messages be acknowledged by secondary messages to prevent premature termination announcements. Their algorithm also uses a secondary static spanning tree to reduce status change messages to the root and to broadcast the termination announcement. The secondary overlay can be (but does not have to be) extracted as a subset of the primary communication topology when it is known in advance. The root is then selected as a central process at a minimal distance to all leaf processes.

When the root process becomes idle, it announces the termination. When a non-root process becomes idle, it sends a STOP message to its parent. A process cannot become idle until it receives a STOP message from all of its children.

During the normal course of the computation, the algorithm counts the outgoing primary messages. A process cannot become idle until it receives a secondary acknowledge message for every outgoing primary message. When receiving a primary message, the receiver, r, may be active or idle.

• When r is active, it acknowledges the reception using a direct ACK s,r secondary message to the sender s.

• When r is idle, it becomes active and sends a RESUME s,r message to its parent.

The parent may receive the RESUME s,r message when it is active or idle. When an idle parent receives a RESUME s,r message from a child, it becomes active, forgets the reception of the STOP message from that child, and forwards the RESUME s,r message to its parent. When an active parent receives a RESUME s,r message from a child, it forgets the reception of the previous STOP message from that child, and sends the ACK s,r to r, following the inverse path from the RESUME s,r message, then r sends ACK s,r to s directly. In effect, delaying the ACK s,r message prevents the root of the subtree containing s and r from becoming idle when a potential RESUME s,r

RR n°9181

message is canceling the STOP-message-induced actions on r's ancestors.

Credit Distribution Algorithms

In a credit distribution algorithm (e.g., HCDA), as originally proposed independently by Huang [START_REF] Huang | Detecting termination of distributed computations by external agents[END_REF] and Mattern [START_REF] Mattern | Global quiescence detection based on credit distribution and recovery[END_REF], an initiator controlling agent starts the computation with C total total credit, and the initiator distributes the credit among processes according to the initial activity of the processes.

During execution, messages carry credit between processes: when a process sends a message, it sends a fraction of its credit along with the message and keeps a fraction of the credit for itself. When a process receives a message, it adds the message-carried credit to its own credit stash. When a process becomes idle, it returns its entire stash of credit to the initiator. From there, the initiator process can detect the termination of all other processes when it again has C total credits. Note that, as usual, an idle process may reset to active as a result of receiving a message. In this case, the process transitioning from an idle to an active state inherits the credit that has been carried in the in-transit message, thus guaranteeing that the initiator misses a fraction of the C total credits for as long as any in-transit or active processes remain. This approach is elegant in theory, but it suffers from multiple drawbacks that hinder its implementation. In non-infinite precision arithmetic, the HCDA algorithm is subject to an underflow problem when dividing the weight into two halves upon message emission. To partially alleviate this problem, Mattern [START_REF] Mattern | Global quiescence detection based on credit distribution and recovery[END_REF] suggests using only credits of the form X = 2 -Y , where Y is an integer, and to encode Y = -log 2 X to represent X. This requires some modifications to the algorithm, outlined below.

• Use 2 -q as the initial local credit, where 2 q-1 < P ≤ 2 q , and total credit is now C total = P2 -q .

• An active node receiving a basic message returns the message-carried credit to the collecting agent, instead of storing it locally, to keep its own summing simple.

Then, all message weights have a weight, 2 -Y , for some Y , and sending a message splits the weight by incrementing Y . However, the complete summation is delegated to the controlling agent rather than eliminated, and many secondary control messages are needed to return the non-locally summed credit to the controlling agent. Another variant suggested in [START_REF] Fokkink | Distributed Algorithms: An Intuitive Approach[END_REF]Ch. 6] allows a node without any remaining credit to create its own credit currency and start a weight-throwing termination detection subcall. Then, that node returns its weight to the initiator when it has become passive and its subcall has terminated. The weights originating from the initiator and from the node must be maintained separately. Again, this variant incurs additional control overhead and extra delays. In Section 4, we discuss how we build upon the basic HCDA strategy to design an algorithm suitable for extreme-scale, distributed HPC systems in a manner that avoids producing a large number of secondary credit return messages and operates without messaging delays.

CDA for HPC

We expand on the classical CDA algorithm with original considerations for HPC platforms executing large-scale, distributed dataflow programs. The major challenge with CDA is the credit attrition resulting from the noninfinite divisibility of the credit representation. Our CDA algorithm strives to achieve a low number of control messages while reducing the disruption of the exchange of primary messages. In our CDA algorithm, credit is represented as integer values (i.e., credit is not infinitely divisible but can be summed efficiently without arbitrary precision arithmetic). During the initial state, credit is distributed equally among nodes. Each process starts with an initial credit of value, C init , known by all. The total amount of credit distributed initially is thus C total = PC init . Note that, in certain applications, not all processes are initially active, and an application-specific policy may have achieved a more optimal initial distribution (e.g., by dividing the credit among initially active processes) but at the expense of losing generality. Initial credit is computationally generated and requires no secondary messages to be distributed.

When a process becomes idle, it returns its credit to the controlling agent with a FLUSH secondary message. This strategy has two drawbacks: (1) it increases the number of control messages, significantly in the worst case; and (2) it accelerates the rate of global attrition of credit in noninitiator processes by removing the flushed credit from circulation (hence increasing the chance that some active process will run out of credit). In primary algorithms executed as a dataflow, the locally visible horizon of tasks scheduled in the runtime can be leveraged to detect that an outgoing message is terminal, that is, the last message sent before a transition to idle.

We observe that sending the whole locally available credit along with pending terminal emissions has multiple benefits: it avoids generating FLUSH messages and maintains more credit available among active processes. When sending a primary message, a process splits its locally available credit (according to different policies detailed below) and "piggybacks" a fraction of the credit onto the message. Because the piggyback is of fixed size (since our credit representation does not grow to remain infinitely divisible), the practical cost of adding the piggyback to primary messages is trivial. However, it is possible that a process that needs to emit primary messages would run out of locally available credit. In this case, the process requests (with a secondary BORROW message) the allocation of supplementary credits from the controlling agent.

The controlling agent counts how many credits have been created during the execution in a counter that grows as necessary, thereby ensuring that the controlling agent will never fail at providing supplementary credits. As a consequence, more credit than is representable by the maximum value of local and message credit may be in circulation in the system. If a noncontroller process receives a message containing more credit than it could accumulate in a single variable without an overflow, its local credit is set to the maximum, and all remaining credit is immediately returned to the controlling agent. For as long as a process is out of credit (e.g., the time period required for the secondary BORROW request to round-trip to the control agent), the process has to delay the emission of all primary messages, since it would otherwise carry the risk of resetting the destination process to active without holding message carried credit.

Running out of credit is a major performance hurdle and should be avoided. To reduce the likelihood of running out of credit, we devise two complementary strategies: (1) the credit division strategy that we employ operates under multiple regimes, and (2) credit borrowing is prefetched.

The minimum credit that a primary message may safely carry is 1. While this strategy reduces the attrition rate at the sender process (by leaving as much credit as possible at the source), if a message reaches a process that has little credit left (e.g., an idle process that had rid itself of all its local credit), then that process will need to borrow credit from the controlling agent and delay the next primary message. Conversely, if a process divides the credit into two halves for every message (as is customary in many CDA algorithms, including HCDA), then local credit declines very quickly (at an exponential rate) with the number of outgoing messages -leading to a high chance of the process running out of credit before it receives credit naturally through its primary message receptions.

We devise a multi-regime strategy that avoids both issues. When a process holds abundant credit (i.e., above a threshold value, C con ) the process employs a credit division strategy to improve the chances that destination processes may carry more message emissions without borrowing. Multiple messages may be sent simultaneously (from the view of the emitter process and independently of the port model of the network) when a task creates multiple successors at remote processes. Each individual successor task may represent an individual emission, yet all are created during the same local step. Message emissions may also appear simultaneous for a process when considering an asynchronous communication system that enqueues non-blocking emissions. Messages may be scheduled from additional tasks that are completing at the local process before the initiation of previously scheduled emissions at that same process. In both cases, instead of dividing the credit by two for every message, credit is divided uniformly among all outstanding emissions when message emissions are simultaneous. We maintain a counter of shares, S, which counts how many shares are known for the RR n°9181 current credit. S is equal to the number of outgoing messages, plus one if the process remains active. Letting C cur denote the current credit amount, each message receives C cur /S credits.

When local credit drops below C con , the allotment of credit per message is modified to carry a fixed amount of credit per message W con . The goal is to conserve the local credit to enable the process experiencing low availability of credit to keep issuing messages with no delays, for as long as possible. Overall, the credit allocation function uses the following formula to set the credit, w i , on an outgoing message, m i , at a process with current credit, C cur , and S shares.

w i = Ccur S if C cur > C con min( Ccur S , W con ) if C cur ≤ C con
In addition, to further avoid delaying emissions, when less than C borrow is available, the process proactively issues a BORROW message to replenish its credit with additional credit from the control process. The amount of credit returned by the control process is C init . In some cases, this may increase the number of secondary BORROW messages, as the process may have received credit (from primary message receptions) before reaching an indivisible credit, but the severe performance penalty resulting from delaying primary messages supports the deployment of this optimization.

Analysis

In this section, we compare the 4C, EDOD, HCDA, and CDA algorithms in terms of their number of control messages. We use two simple applicative kernels for this comparison: (1) the token ring, which is the archetype case study for distributed algorithms; and (2) tree-based synchronous computations, which are a good approximation of the target applications used in Section 6.

Token ring

The token ring is a kernel widely used to assess the performance of distributed algorithms [START_REF] Misra | Detecting Termination of Distributed Computations Using Markers[END_REF][START_REF] Martin | Distributed mutual exclusion on a ring of processes[END_REF][START_REF] Défago | Total Order Broadcast and Multicast Algorithms: Taxonomy And Survey[END_REF]. Informally, it consists of several steps, with a token randomly moving from one process to another at every step, and a random number of steps. We use the following instantiation.

• The token is initially owned by process 0.

• With a fixed probability of q < 1, the token owner draws a process number randomly and uniformly in [0, P -1] and sends a message (the token) to that process. The algorithm stops with a probability of 1 -q.

The expected number of steps (token moves) of the algorithm is 1 q . At each step, the token owner performs some computation, the precise length of RR n°9181 which is not important but is assumed to be long enough so that all control messages of the termination detection algorithm are processed before the next step begins. In other words, we can view the steps as synchronized, with the termination algorithm detecting termination (or not) at the end of each step.

The token ring mimics the termination pattern of an application that ends with a linear chain of tasks, the length of which is data dependent. Our results are shown below in Theorem 1.

Theorem 1. The expected number of control messages of 4C, EDOD, HCDA, and CDA for the token ring is the following:

• E(4C) ≥ 1 q 2P log(P) + P + o(P) • E(EDOD) ≥ 1 q × 3 log(P) + P + o(P) • E(HCDA) = 1 q + 2 log(C init )q + P + o(P) • E(CDA) ≤ 2P
We see that EDOD is more efficient than 4C at each step, and that CDA is the clear winner as soon as the token circulates at least P times.

Proof. At each step of the token ring algorithm, the sender node makes an active-to-idle transition, while the receiver node is awakened by the token message and makes an idle-to-active transition. Because we assume the steps do not overlap, these are the only two transitions during the step, and all the other processes remain idle.

For the 4C algorithm, the sender initiates a chain of messages by notifying its parent in the control tree. There are two cases, described below.

• If the receiver is not an ancestor of the sender in the control tree, it will notify its parent, which in turn will notify its parent, thereby eventually reaching the root. If the current step is not the last step, the root will detect that the current wave has failed (because not all nodes have reported being idle) and will propagate this information down to tree to all processes via a descending wave; if this is the last step, the root will detect termination and send the final descending wave; in both cases, the cost is P -1 control messages.

• If the receiver is an ancestor of the sender in the control tree, the chain of messages from the sender to the root will be blocked by the receiver. But this latter event has a small probability, because there are at most log(P) nodes in the path from the sender to the root. Hence, the probability of the receiver belonging to that path is at most log(P) P . Altogether, the expected number of control messages per step is at least (1 -log(P) P )(P -1) + log(P) P × 1 = P + o(P)

RR n°9181

Adding the cost, P -1, of the final notification broadcast, we get the result for E(4C), since the expected number of steps is 1 q . For the EDOD algorithm, we have the following analysis.

• Initially, every node transitions from active to idle, either immediately or after sending the first message for the initiator, and sends a message to its parent in the control tree; therefore, there are P -1 messages.

• For each token message at each step, an acknowledge message is sent by the recipient to the sender. It goes through a chain of resume and acknowledge all along the unique path in the control tree connecting both nodes. number of control messages is equal to the distance between both nodes in the control tree. The average distance between two nodes in a complete binary tree of P nodes is asymptotically 2 log P [START_REF] Parhami | Exact formulas for the average internode distance in mesh and binary tree networks[END_REF]. As a side node, we see that this average distance is of the same order as the diameter of the tree, which can be explained by the fact that the majority of nodes are leaves of the tree (see [START_REF] Parhami | Exact formulas for the average internode distance in mesh and binary tree networks[END_REF] for further details).

• We have to add the stop messages, propagated by the sender up to the tree, which leads to log P additional messages per token message. Altogether, the overhead is 3 log P per step.

Adding the cost, P -1, of the final notification broadcast, we get the result for E(EDOD). Finally, we discuss the number of control messages for the credit distribution algorithms. For HCDA, we count a message (to return the credit) every step and two messages (borrowing request and extra credit) every log(C init ) steps, when the credit piggybacked in the primary message runs out. For CDA, this means the following.

• After the first step, process 0 (the source node) becomes idle after the token message is sent, and it transfers all its current weight, C init , into the token message and has nothing to return to the controlling agent. All nodes except the source node were active and became idle during the first step, hence they return their total weight to the controlling agent, which amounts to P -1 control messages.

• While the token iterates during the following steps, the sender has weight, C init , and transfers it into the message, and then it has zero weight and does nothing more. The recipient had weight, 0, and gets C init from the message.

• Upon termination, the recipient sends its weight, C init , back to the controlling agent.

Altogether, the overhead is P messages (out of which P -1 are sent during the first step), hence the result for E(CDA) when adding the cost of the last termination broadcast. An important distinction for CDA is that the total number of control messages is independent of the number of steps.

Non-deterministic binary trees

We consider now the projection operation in 1-dimensional trees described in Section 2. In practice, we can model such an operation with a task graph that unfolds a binary tree, each node having two children with some probability, and being a leaf otherwise. Since an exact analysis with arbitrary task weights is out of reach, we present a simplified scenario to evaluate the average performance of the four algorithms. The simulation works as follows: first, we precompute some application trees with the following algorithm:

(1) Start with a complete tree of height L min = 3.

(2) For each leaf, at level l with probability λ l , refine by replacing the leaf with a complete subtree-the height of which is drawn uniformly and at random between 2 and 5 (i.e., we add between 2 and 30 new nodes).

(3) Repeat the last step on all new leaves until no leaf is refined.

(4) Crop the tree if its height exceeds L max .

The tasks of the tree are labeled using a breadth-first order: task 0 is at level 0, and tasks 1 and 2 are at level 1, and so on. We generated different sizes of trees using the following parameters: small trees with λ = 0.8 and L max = 30, medium trees with λ = 0.9 and L max = 50, and big trees with λ = 0.93 and L max = 60.

For the simulation, we consider that all tasks at a given level, l, are processed at time, l. We have two different mapping strategies for mapping tasks to processes: (1) a round-robin mapping, where task x goes to process x mod P; and (2) a random mapping, where task x goes to a process uniformly drawn in [0, P -1].

We compute the messages sent by the application at each step (all tasks at a level in the tree), and determine whether the processes become active or idle at the end of the step. When a process was active and is again active at the end of the step, we model the inherent distributed aspect of the algorithms using three different models:

• S instant : The node does not transition to idle during the step, it remains active throughout. This corresponds to the case where computations and communications are instantaneous, thus a node knows in advance whether it will stay active or not.

• S local : The node transitions to idle before returning to active, unless there is a message to itself. This corresponds to the case where communications are very slow compared to computations, all messages are received at the end of the step, so a process transitions to idle because it cannot know in in advance whether it will stay active or not.

• S load : The node transitions to idle before returning to active only if it has no message for itself and if its load is smaller than all the loads of the nodes that send a message to it: this is because in that case, it terminates computing before receiving any load from the other guys. This corresponds to the case where computations are long and messages takes very short time. We define the load to be equal to the number of messages received at the previous step (each of them implying the execution of a task, this corresponds to assuming that all tasks have the same weight).

To compare the performance of CDA to other algorithms, we compute the number of control messages sent by each algorithm, as detailed below.

• HCDA and CDA: all messages carry credits, so there is no control message -except when one process becomes idle and needs to return its credit to the controlling agent (flush), or when it does not have credit anymore and needs to send a message to the controlling agent to continue (borrow). Each time we detect that a process needs to flush or borrow, we add one control message. Otherwise, when processes transition from idle to active or from active to idle, we do not count anything, as these algorithms do not send messages for simple transitions.

• 4C: once the list of messages (sent during a step) is computed, we go through the list of all processes in descending order. If a process becomes idle, we check if it belongs to the wave. If it does not, it is added to the wave; if the process has children, they also belong to the wave. By going through the processes in descending order, we ensure the wave goes as high as possible in the control tree. Each time the root belongs to the wave, we account for 2(P -1) messages (2× the number of edges in the control tree).

• EDOD: each time a process, p i , transitions from idle to active, it means that it received messages from a set of processes, S. We then compute the union of all paths from p i to each one of the processes in the set S. Finally, we sum the number of edges in that union of paths, which accounts for the number of control messages sent at this step by process p i . When a process, p i , transitions from active to idle, we check that its whole subtree is composed of idle processes at the end of the step. In that case, we account for one control message that goes up in the control tree; there are n messages total, where n is the size of the subtree, because each node of the subtree is the root of an idle subtree itself.

Figure 2 presents the number of control messages for all algorithms. We had to use a logarithmic scale on the Y-axis to report a range of different numbers. The data presented is based on a big tree (but results are similar on smaller trees) using an initial credit, C init = 2 32 . First, these simulations show that CDA dramatically outperforms HCDA. Interestingly, the only occurrences of BORROWs for CDA are when the mapping is random and there are only a few processes. In this case, the processes may receive a lot of messages, thus a lot of tasks to execute, and thus a higher number of messages to send afterward. With the credit reducing quickly at the beginning because there is a good probability that a process is idle in the first steps, and there may be too many messages to send compared to the credit. Still, the number of BORROWs is -on average -null, especially when using round-robin mapping. The only overhead in terms of messages added by CDA comes from the number of flushes (when a process becomes idle and has no message to send). When using round-robin mapping, the number of flushes per process is less than the number of control messages sent by the 4C algorithm (on average for the first figure). However, when we set the mapping to be random, 4C proves to be more efficient than CDA when P > 100. Between random and round-robin mapping, the number of control messages for CDA does not change much, whereas random mapping drastically reduces the number of control messages for 4C.

Overall, we expect CDA to send less messages than 4C, in particular when the number of processes increases. Looking at the top-right plot in Figure 2, where the model is S load and the mapping is round-robin (achieving more load balance than random), the number of flushes per process tends to stay constant when the number of processes increases, whereas 4C produces more messages.

Experiments 6.1 Implementation

To evaluate the termination detection algorithms, we implemented them in the Parallel Runtime Scheduling and Execution Controller (PaRSEC), a micro-task system for distributed environments [START_REF] Bosilca | PaRSEC: Exploiting Heterogeneity to Enhance Scalability[END_REF]. The Modular Component Architecture (MCA) of PaRSEC enables dynamic module selection to provide desired functionality. We extended PaRSEC to integrate a new termination detection framework capable of providing support for multiple termination detection strategies. We interfaced the termination detection component with: (1) the scheduler to determine if there is local activity; (2) the domain-specific language (DSL) to determine if there is potential future activity; and (3) the communication engine to stay informed of outgoing and incoming messages and to provide termination detection-specific messaging. The communication engine is enhanced to allow the termination detection module to piggyback information within primary messages (as needed to implement CDA). Taking advantage of this MCA framework, we designed and implemented support for all termination detection algorithms studied.

As stated previously, many applications can detect their own termination. The DSL or the algorithm can "pre-compute" the entire set of local work, or the termination may occur at a single terminal node of the workload task graph (e.g., fork-join parallelism). For such applications, we provide the local and announce termination detection modules that simply inform the runtime of the application-detected termination. The dynamic termination detection algorithms are implemented in additional modules, which are then selected by the DSL when the application is dynamic.

Benchmarks

To evaluate the different algorithms, we implemented a couple of micro benchmarks into one of the PaRSEC DSLs, a dataflow language, called the Parameterized Task Graph (PTG). The micro benchmarks stress termination detection with different cases: the token-ring algorithm, which is analyzed and described in Section 5.1, and the projection operation on a 1-D tree, which is described in Section 2 and analyzed in Section 5.2.

The token ring benchmark aims to emulate an application where the workload moves across processes during the execution (e.g., computing the cumulative distribution function -CDF -of another function provided as a k-dimensional tree). For CDF, the input must be summed at each leaf to create the leaves of the target function; leaves with insufficient data precision may be further refined by spawning additional local tasks. To emulate this behavior, we define a probability of branching during the circulation of the token: while the main token continues circulating (emulating the sum of leaves on the input tree), at each node, with probability q b , additional tokens that spawn local refinement leaves are created. This benchmark represents a class of dynamic applications where a pipeline of work terminates at a singular (or a limited) number of processes, simultaneously.

The projection benchmark approximates the e -2x function in the domain [-10, 10] with a variable precision threshold (the finer the precision, the deeper the tree representing the approximation of the function). As is done in MADNESS [START_REF] Harrison | MADNESS: A multiresolution, adaptive numerical environment for scientific simulation[END_REF], tree nodes are distributed following a heuristic that aims to balance the load while preserving some locality. Nodes at depth d < log 2 (P), where P is the number of processes, are randomly assigned to a process, while nodes at depth d ≥ log 2 (P) are assigned to the same process as their closest ancestor with the same depth. This workload is representative of the class of applications where multiple processes enter termination simultaneously.

Results

Experimental Setup

All experiments were conducted on Argonne National Laboratory's Mira supercomputer -a Blue Gene/Q system with 48 compute racks and 786,432 total compute cores (Power7) running at 1.6 Ghz. All experiments used a single midplane (512 compute nodes), and each compute node features 64 hardware threads. We deployed up to 32 MPI processes per compute node; every MPI process has a computation thread and a communication thread, each bound to their own hardware thread, hence 32 MPI processes across 64 hardware threads. We ran each experiment 20 times and report all measurements using Tukey Boxplots -the boxes delimitate from the 1st to the 3rd quartile, and whiskers denote the lowest (respectively highest) datum still within the 1.5 interquartile range of the lower (respectively highest) quartile.

Token Ring

First, we consider the Token Ring studied in Section 5.1. Figure 3 presents, for each termination detection algorithm, the number of control messages (i.e., secondary messages not issued by the application) and the time between the last transition to Idle and the last process that detected termination (detection latency). At 16,384 processes, EDOD introduces so many control messages on the critical path that the benchmark fails to complete within the maximum runtime limit (60 s). This result reinforces the notion that comparing termination detection algorithms based on the number of control messages only is not enough; their differences are more subtle. It also highlights a critical difference between EDOD and 4C: both introduce a comparable number of messages in this case, but the impact of these messages on the execution time is wildly divergent. The drastic impact on EDOD is due to congestions introduced: as the token circulates, each process uses the tree to send the acknowledge and resume messages to the source of the token. The links of the tree are quickly overloaded with control messages as they compete with the application messages for network resources. Comparatively, at most one wave is ongoing at each instant with 4C. Although many serialized waves are necessary, they do not compete simultaneously for the network resources. CDA and HCDA behave the best in this setup. For CDA, the credit circulates with the token without diminishing significantly, and very few control messages are necessary (about 2 per process, see Section 5). For HCDA, although the credit expires every 32 steps, the number of control messages is still linear with the number of steps and is smaller than for EDOD or 4C at scale. CDA, HCDA, and 4C behave efficiently in terms of detection latency, while the control communication tree of EDOD is overloaded with control messages, resulting in high latency.

Projection Operation

Second, we looked at the projection operation. Because of its naive credit management strategy, HCDA suffers from scalability issues, and we could not study a large problem with HCDA. To illustrate this, we compared the number of control messages introduced by HCDA and CDA over the projection operation on 16,384 processes and variable precisions (Table 1).

The HCDA algorithm quickly suffers from attrition due to early flushing and bad credit splitting heuristics (as explained in Section 5.2), resulting in many more FLUSH and BORROW messages than CDA. As the precision goes finer, the problem size increases, and a higher number of leaves appear in the projected tree. For each leaf, there is a potential for a flush message, forcing the processor that created the leaf to flush its credit and borrow more when a subtree is subsequently discovered. The number of control messages grows up to 100× larger in the HCDA algorithm compared to our CDA algorithm. Moreover, the BORROW messages in the CDA and HCDA algorithms are in the critical path of the execution, and, because their number explodes for the HCDA algorithm, the centralized agent that must serve them is quickly overloaded upon attrition. This is why attrition must be avoided to obtain an efficient CDA implementation. Because of this, runs of the HCDA algorithm would not complete in a reasonable time at a of 10 -13 on the platform we used. Whereas, by avoiding attrition, the optimized CDA has no measurable impact on the overall execution time of this benchmark, similar to the other algorithms studied (EDOD and 4C). Hence, for the rest of the evaluation, we discard HCDA and consider only EDOD, 4C, and CDA.

Figure 4 shows the number of control messages injected by each termination detection algorithm and the impact on the detection latency for the projection operation. Note that, from the detection latency perspective, the three algorithms exhibit similar performance despite a drastically different number of control messages. EDOD injects control messages for each application message, even before any process enters the idle state. This significantly impacts the number of control messages, which is orders of magnitude higher than for CDA and 4C. Because these messages compete with each other on the links of the underlying control tree, contention becomes critical, and the detection latency suffers.

Although 4C behaves much better than EDOD in terms of control messages, it still creates many times more messages than CDA at large scale. Note that the scales on both axes are logarithmic due to the significant difference in the number of messages between the different algorithms, which is consistent with our simulations. At smaller scale, there are problem sizes for which 4C introduces less control messages than CDA. The benchmark creates parallel work that is evenly distributed among the different processes. As a consequence, the waves of 4C are relatively slow to reach the root (all processes have to switch to the idle state at least once for a wave to reach the root), and the number of waves remains small (the number of waves is the number of control messages divided by twice the number of processes). In the case of CDA, almost all control messages are FLUSH messages. In this application, processes computing leaves have no further use for the credit they received when creating the leaves. Thus, they initiate a flush every time they become idle after processing a leaf. The FLUSH messages introduced by CDA are away from the critical path, and only BORROW messages may delay the execution. Similarly, the waves of 4C do not prevent the application from progressing normally. For both algorithms, the noise introduced in the system does not measurably degrade the performance.

CDA: Risk of Borrowing and Messages Delays

We detail our study of how CDA behaves during the projection operation in terms of control messages that have an impact on the application (e.g., the BORROW messages that prevent primary messages from being delivered in a timely manner). Unlike 4C or EDOD, CDA can slow an application, because it may run out of divisible credit. Indeed, if a process needs to send a message but no divisible credit is locally available, the emission must be delayed until credit is acquired -either from the root through a borrow or from an incoming message. In Figure 5, we show, for a set of projections, how many times an application message emission was delayed and how many times processes issued a borrow order. First, one can see that these two measures are strongly correlated. This is to be expected as a borrow order is issued when a process runs out of credit. Second, one can also see that, depending on the number of processes (hence depending on the number of tasks per process), the number of borrows and delayed messages vary significantly. On one hand, as the scale increases, the number of tasks per process decreases (for a fixed problem size); thus, the number of messages and the credits required to initiate messages also decreases. On the other hand, at small scale, each process executes more tasks that are successors of tasks from remote predecessors, and thus receives more credit from the application messages. This creates a trade-off that is beneficial at each extrema but detrimental at the middle. However, even when the number of borrows is maximal (at 2,048 processes), no process initiates more than one borrow over the course of the execution. Thus, despite producing a large number of delayed messages, that single disruption has a negligible impact on the entire application runtime.

Related work

In [START_REF] Tseng | Communication pattern based methodology for performance analysis of termination detection schemes[END_REF], a method to more precisely define the metrics of efficiency for distributed termination detection is proposed. We leverage this method in our theoretical and simulation-based analysis.

Termination detection has been studied extensively from the theoretical perspective: [START_REF] Peri | Improving the efficacy of a termination detection algorithm[END_REF] demonstrates that different classes of detectors are equivalent through automatic transformations; see Ch. 6 of [START_REF] Fokkink | Distributed Algorithms: An Intuitive Approach[END_REF] and Ch. 9 of [START_REF] Ghosh | Distributed Systems An Algorithmic Approach[END_REF].

Wave termination detection algorithms include [START_REF] Huang | Termination detection by using distributed snapshots[END_REF], based on distributed snapshots, and [START_REF] Wang | A general model for detecting distributed termination in dynamic systems[END_REF], designed for asynchronous wide-area networks by combining a reduction tree with a logical ring. Delay optimal algorithms include [START_REF] Mittal | Messageoptimal and latency-optimal termination detection algorithms for arbitrary topologies[END_REF] and [START_REF] Nihar | An efficient delay-optimal distributed termination detection algorithm[END_REF], and we compare one that is representative to this work. Weight throwing, or distributed credit algorithms, have been extensively studied theoretically: [START_REF] Stephen | Starting with termination: A methodology for building distributed garbage collection algorithms[END_REF] proposes to use them to implement garbage collection mechanisms; [START_REF] Livesey | The doomsday distributed termination detection protocol[END_REF] introduces the Doomsday termination detection protocol that deals with migrating tasks; [START_REF] Garanina | Distributed termination detection by counting agent[END_REF] uses a mobile agent to count the weight remaining in the system; [START_REF] Mishra | A weight throwing and diffusing computation based approach for termination detection in manets[END_REF] and [START_REF] De | A new termination detection protocol for mobile distributed systems[END_REF] consider the particular case of mobile networks; and [START_REF] Tseng | Detecting termination by weight-throwing in a faulty distributed system[END_REF] considers resilient approaches to these algorithms.

Few works compare, experimentally or practically, the different algorithms to evaluate the behavior in average or real-world conditions. In [START_REF] Demara | Tiered algorithm for distributed process quiescence and termination detection[END_REF], this comparison is conducted over a simple benchmark consisting of 100 randomly generated nested graphs of tasks. Here, we studied the implementation in a production-quality distributed system, at scale, for benchmarks representing real applications.

Conclusion

This paper revisits distributed termination detection algorithms in the context of HPC applications, motivated by the need to efficiently detect termination of work flows for which the total number of tasks are data-dependent and, hence, not known until during execution. We introduce an efficient variant, CDA, of the credit distribution algorithm, and compare it, both theoretically and practically, to the initial credit distribution algorithm, HCDA, and to two other termination detection algorithms, 4C and EDOD. On the theoretical side, we analyze each algorithm for simplified task-based kernels and show the superiority of CDA in terms of the number of control messages. On the practical side, we provide a highly tuned implementation of each termination detection algorithm within PaRSEC, and compare their performance for a variety of benchmarks reflecting scientific applications that exhibit dynamic behaviors. These experiments reveal the dramatic shortcomings of the initial HCDA algorithm and corroborate the superiority of our new CDA algorithm in terms of control messages, global overhead, and latency detection.

Future work will see the integration of the proposed algorithm in future releases of the PaRSEC runtime and a study to expand the number of experiments with various task-based HPC workflows in an attempt to better understand the impact of termination detection algorithms on different types of applications.

Figure 1 :

 1 Figure 1: Sample application: 1-dimensional tree whose refinement locally depends on the slope of the target function.

Figure 2 :

 2 Figure 2: Number of control messages per process for all algorithms (4C, EDOD, HCDA and CDA) for a 202007-task tree. The first row uses a mapping while the second row uses a random mapping.

Figure 3 :

 3 Figure 3: Random Walk, with branching probability, q b = 0.1.

Figure 4 :

 4 Figure 4: Projection operation with threshold of 10 -13 .

Figure 5 :

 5 Figure 5: CDA: Number of borrows and number of messages delayed during a projection operation, threshold: 10 -13 .

Table 1 :

 1 Average number of control messages for HCDA and CDA (projection operation with 16,384 processes).

				Projection Precision
		10 -7	10 -8	10 -9	10 -10	10 -11	10 -12
	HCDA	34,388	58,638	69,542	437,542	659,761	2,578,376
	CDA	30,154	25,038	25,767	26,338	24,468	27,562

RR n°9181

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Acknowledgements

This research was supported by the Exascale Computing Project (17-SC-20-SC), a collaborative effort of the U.S. Department of Energy Office of Science and the National Nuclear Security Administration. This research was supported partly by the NSF project #1450300.


M K Iyer

G Parthasarathy

K.-T Cheng

Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver

  L'archive ouverte pluridisciplinaire

Introduction

Checking the satisfiability (SAT) of complex, quantifierfree first-order logic formulas, is an important problem in verifying register-transfer level (RTL) hardware designs. Though Boolean SAT solvers have demonstrated impressive advances in the last decade, quantifier-free arithmetic is still expensive to solve in the Boolean domain [START_REF] Brinkmann | RTL-Datapath Verification using Integer Linear Programming[END_REF].

There have been several attempts to integrate decision procedures for Boolean and integer domains into a combined decision procedure(CDP) e.g.,the stanford validity checker (SVC) [START_REF] Barrett | Validity Checking for Combinations of Theories with Equality[END_REF], the integrated canonizer and solver (ICS) [START_REF] Filliâtre | ICS: Integrated Canonization and Solving[END_REF], and UCLID [START_REF] Seshia | Hybrid Sat-based Decision Procedure for Separation Logic with Uninterpreted Functions[END_REF]. There has been some work on an orthogonal approach where the Boolean and integer domains are considered to be domains of different sizes and values. The resulting problem is solved by a specialized solver e.g.,CAMA [START_REF] Liu | CAMA: a multivalued satisfiablity solver[END_REF], or by a general finite-domain solver e.g.,LPSAT [START_REF] Zeng | LPSAT: A Unified Approach to RTL Satisfiability[END_REF]. All these methods have performance problems on RTL circuits.

Recently, HDPLL [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF], and DPLL(T ) [START_REF] Ganzinger | DPLL(T): Fast Decision Procedures In CAV[END_REF] independently proposed a new approach by combining decision theories under a branch-and-bound DPLL-style [START_REF] Davis | A Machine Program for Theorem Proving[END_REF] framework. Both approaches cited the importance of constraint propagation and conflict-based learning to maintain efficiency. HDPLL used finite-domain constraint propagation (FDCP) to integrate Boolean SAT and integer fourier-motzkin elimination (FME) into a hybrid DPLL procedure. Heuristics for conflictbased learning were used to prune the combined search space. DPLL(T ) combined the theory of Boolean logic with the the-ory of uninterpreted functions with equality (EUF). There is no mechanism for learning across theories in DPLL(T ), and it can handle only comparisons with equality, which makes it currently unsuitable for RTL satisfiability.

In this paper, we address an important problem in any DPLL-based combination of decision theories -conflictbased learning. In general, it is desirable to find explanations for conflicts across theories. It is also desirable to represent these explanations in a form that can be efficiently used for constraint propagation. We present an efficient method of analyzing the combined implication graph of both sub-theories to find unique implication points (UIPs) [START_REF] Marques-Silva | GRASP -A Search Algorithm for Propositional Satisfiability[END_REF]. We also present a lazy implication data-structure for efficient constraint propagation on these UIPs across theories.

The rest of this paper is organized as follows: First, we describe some basic concepts of modern DPLL and the HDPLL algorithm proposed by [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF] in Section 2. We describe a systematic approach to conflict-based learning on the combined implication graph and resolution graph of HDPLL in Section 3. We then describe data-structures that allow us to learn hybrid learned clauses on both the integer and Boolean domains in Section 4. Finally, we compare our approach with some state-of-the-art CDPs -CVC-Lite, ICS, and UCLID for SAT on RTL circuits in Section 5.

Background

In this section, we briefly introduce some of the main concepts, relevant to this work. We begin with some definitions.

A finite-domain d(v), is a complete mapping from a variable v to a finite set of integers. A Boolean variable has a domain of {0, 1}, and a word variable of bit-width w, has a integer valued domain of {0,...,2 w -1}. A literal, is the appearance of a variable in a clause. A clause is a disjunction of Boolean literals. A hybrid clause is a disjunction of Boolean and word literals. A finite-domain (FD) constraint is an inequality over constant coefficients a i of arbitrary sign, word (Boolean) variables x i with a fixed domain d(x i ) ({0, 1}) of the form:

∑ i a i • x i ≥ r, a i , r, x i ∈ I
A literal l i /¬l i of a Boolean variable v i denotes its value as 1 or 0. A word-literal of a word-variable v j is associated with a range b j as a pair, l j b j /¬l j b j . A positive literal in the pair, denotes that v j has range b j , and a negative literal in the pair denotes that v j has values in d(v j )\b j , i.e., v j should not have any value in range b j .

Efficient Implications

The DPLL algorithm [START_REF] Davis | A Machine Program for Theorem Proving[END_REF] for Boolean SAT problems is based on case-splitting on variables and Boolean constraint propagation (BCP). Given a set of assignments, BCP finds implications or additional assignments, that must hold for the problem to be consistent. BCP is also used to determine when the search has moved outside the solution space i.e., a conflict.

BCP is the most frequently used procedure in any DPLL style algorithm. Therefore, a clause should be evaluated for an implied value, only when it is guaranteed that an implication will occur. This is the basic idea of lazy implications. It uses the data-structure called the two-literal watching scheme and shown in Figure 1. On average, it yields significant improvement in performance [START_REF] Moskiewicz | Engineering an Efficient SAT Solver[END_REF][START_REF] Zhang | An Efficient Algorithm for Unit Propagation[END_REF], on hard problems with large clauses.

Variable Data Structure Watch Pointers

Watched Literal

Watch pointers

Clauses

T T 5 v H H T T 1 v H H 3 v 5 v 1 v 5 v 2 v 4 v 1 v 6 v 5 v 1 v 7 v 1 v 5 v i v H/T

Figure 1. Data-structures for Literal Watching

Each clause initially has two pointers pointing to two distinct unassigned literals. These pointers are kept on the variable corresponding to these literals, and are called watched pointers. The two watched pointers on a clause move in opposite directions and schedules implications using the following rules [START_REF] Moskiewicz | Engineering an Efficient SAT Solver[END_REF]:

1. A watched pointer moves to the next unassigned (unknown) literal when its literal evaluates to false. 2. The pointer does not move when the literal evaluates to true, since the clause is satisfied i.e., no further implications can be derived from it. 3. When both pointers point to the same literal on a clause, then an implication is scheduled, since all other literals except the current literal are false.

Conflict-based Learning from Implications

Given a sequence of value assignments in DPLL, we can construct a graph that represents the causal relationship between value assignments, called the implication graph. The implication graph is a directed graph IG(N, E), where N is the set of nodes and E is the set of edges. A node n ∈ N represents a value assignment to a variable. A directed edge e ∈ E exists from nodes n a to n c , if n a is (part of) the value assignment(s) that implies the value assignment n c . A conflict is represented by a unique node in the IG.

A set of nodes (cut) in IG, covering all paths to the conflict node gives a conjunct of value assignments( V i l i ), that will cause the conflict. The negation of this is a disjunct ( W i ¬l i ) that must be true for the conflict to be avoided. This is added to the problem as a conflict-avoiding or learned clause. The process of finding and using these learned clauses is called conflict-based learning. A unique implication point (UIP) [START_REF] Marques-Silva | GRASP -A Search Algorithm for Propositional Satisfiability[END_REF] is a cut in IG that is a dominator for all paths in IG to the conflict, and is smaller than any other non-UIP cut. An example will be shown in Figure 3.

Fourier-Motzkin Elimination

Fourier-motzkin elimination (FME) [START_REF] Dantzig | Fourier-motzkin elimination and its dual[END_REF] is an efficient method to check satisfiability of a set of integer inequalities. FME iteratively eliminates a variable from a set of constraints with n variables, to find an n -1 dimensional projection of the constraint set. The Omega test by Maslow et al., [START_REF] Kelly | The Omega Calculator and Library v1.1.0[END_REF] uses fourier-motzkin with normalization and rounding for testing the satisfiability of a set of integer constraints. This corresponds exactly with the Boolean notion of resolution [START_REF] Hooker | Logical Inference and Polyhedral Projection[END_REF]. Omega is used in HDPLL as the decision procedure for the theory of integer arithmetic.

Similar to the implication graph, we can construct a directed graph called a resolution graph RG(C, E). It represents the causal relationship between resolution steps in FME. Each node c i ∈ C represents a constraint. An edge e j ∈ E, exists between two nodes, c k and c l , if c k was used to form the resolvent constraint c l . An example will be shown in Figure 4. We can analyze the resolution graph to find the set of constraints that resolve to a conflict. This yields a powerful conflict-based learning technique, which is described in Section 3.2.

Hybrid DPLL Algorithm

We now describe the main elements of the HDPLL algorithm proposed in [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF], which is reproduced in Figure 2. The procedure Decide() makes decisions only on Boolean variables. The procedure FDdeduce() performs hybrid consistency checking using FDCP similar to BCP in DPLL. The set of assignments to FDdeduce() can be literals appearing purely in Boolean clauses, or in integer constraints, or domain changes on word-level variables. analyze_fdcp(), which is the conflict analysis procedure, does heuristic conflictbased learning based on incomplete analysis of the implication graph. If the Boolean decision procedure does not find a conflict, the procedure FME() is called for a final consistency check on the data-path. If FME() returns UNSAT, an analysis procedure called analyze_fme() is called to find a set of conflict causes. This corresponds to a subset of assignments on a fixed cut in the implication graph [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF]. This subset is found by iteratively solving the data-path relation using FME. If the learned clause conflicts with the unique implications, the problem is UNSAT. If not, HDPLL backtracks non-chronologically and continues search.

As we have noted, the conflict analysis in earlier work was based on heuristics that did incomplete analysis of the implication graph. They used conflict-avoiding clauses with only Boolean literals, by setting a fixed cut in the implication graph, since they did not have a method for efficient UIP clause learning across domains.

In this work, we concentrate on improving the procedures analyze_fdcp() and analyze_fme() to enable learning true UIP clauses [START_REF] Marques-Silva | GRASP -A Search Algorithm for Propositional Satisfiability[END_REF] by a complete analysis of the implication and resolution graphs. We shall show that this is more efficient than incomplete analysis. Next, we describe conflictbased learning across theories in HDPLL.

Hybrid Conflict-Based Learning

In this section, we describe the details of the new conflictbased learning in the combined Boolean and integer domain with FDCP and FME. We describe this as modifications to the procedures analyze_fdcp() and analyze_fme() in Figure 2. The fundamental idea behind the new learning procedure is that the implication graph from FDCP and the resolution graph from FME are combined into a single graph for conflict analysis.

Conflict Learning in HDPLL

We use FDCP to imply values both in the data-path and the control from any decision in the Boolean control. This enables us to construct an implication graph that can be used for conflict-based learning. The graph is implicitly represented by the stack of assignments made so far, similar to modern SAT solvers. The procedure analyze_fdcp() in the HDPLL algorithm (Figure 2), performs conflict analysis by implicitly tracing the implication graph to find the UIP as in standard Boolean conflict-based learning e.g., [START_REF] Marques-Silva | GRASP -A Search Algorithm for Propositional Satisfiability[END_REF].

However, there are some complications introduced by FDCP. Finite-domain constraints with word-level variables can have multiple, monotonically decreasing range changes. Therefore, a variable v i , with a range l, m , can appear with a different range j, k , where, either j < l or k < m, in the current implication graph. We refer to multiple appearances of word-variables in the implication graph as variable incarnations. The procedure keeps track of these incarnations efficiently by keeping a stack of evolving variable states of the variable. The variable state contains the implying constraint for each incarnation, the index of the decision at which it was implied (or decision level), and the incarnations of the variables in the implying constraint. Let us take the example shown in Figure 3(a) with the proposition, {b 3 = 1}. The proposition is UNSAT. The implication graph for the example is shown in the Figure 3(b). We find by implication of the proposition, that b 1 = 1 and b 2 = 1, which produces conflicting ranges w 5 = 5, 6 and w 5 = 3, 4 . We can see that a value assignment in the Boolean logic resulted in a conflict on a data-path variable. Now, if we trace through the implication graph from the conflict site, we find that the UIP is (¬b 3 ). Since this conflicts with the proposition, we deduce that it is UNSAT. The method in [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF] would find the clause (¬b 1 ∨¬b 2 ), and then find the clause (¬b 3 ), before deducing that the proposition is UNSAT.

If no conflict is detected during regular Boolean decision making and FDCP, we must do a final consistency check using FME as shown in Figure 2. If FME returns a conflict, we use an algorithm that extracts information from FME to find a conflict-avoiding learned clause. This is described next.

Conflict Based learning in FME

In this section, we describe a method for tracing the resolution graph from FME for conflict-based learning in HD-PLL. Recall that FME is called when the Boolean theory and FDCP are consistent.

We can unite the implication graph from FDCP and the resolution graph of FME (see Section 2.3) by adding edges between the shared variables of the integer and Boolean theo-ries (e.g.,Boolean outputs of comparators etc). This results in a combined implication-resolution graph HG = (IG ∪ RG ∪ {GLUE}). {GLUE} is a set of edges added to connect IG and RG. A directed edge gl ∈ GLUE exists between a Boolean variable assignment b i in IG and constraint c j in RG, if b i enforces c j to be true, and vice-versa. Intuitively, the set of constraints and assignments on an arbitrary cut in HG that covers all paths to the conflict, are the causes for the conflict. This motivates the idea that we can extract learned information from UNSAT calls to FME in HDPLL, by analysis of the unified implication-resolution graph.

Consider the example in Figure 3(a). Assume that we do not do any constraint propagation in the data-path, which gives us a partial implication graph with assignments, b 1 = 1, and b 2 = 1, shown in the top half of Figure 4. The datapath problem is passed to FME, which performs a series of variable elimination steps. This is represented as a resolution graph as shown in the lower half of Figure 4. The problem given to the FME procedure is the set of constraints marked 1, 2, 3, 4 in the figure. The edges from b 1 and b 2 to constraints 2 and 1 respectively are the additional edges, {GLUE}, added to unite the two graphs. In the example, FME eliminates variable w 2 from the constraints 3 and 4 to get constraint 5. When variable w 4 is eliminated by substituting w 4 = w 5 + 2, in constraint 1, we get a conflict since the resolvent is the empty constraint -2 ≥ 0.

Resolution Graph

First UIP Cut Implication Graph The above method replaces the procedure analyze_fme() in Figure 2. We trace through the resolution graph from the conflict resolvent, to find the smallest set of assignments that are responsible for the generation of that conflict resolvent i.e., a cut in HG. There may be other constraints on this cut (constraints with no incoming edges) that contribute to the conflict. These constraints enforce the functionality of datapath primitives. We do not need to add these constraints to the set of conflict causes, since these constraints always have to be true for the proposition to be true. If we trace through the resolution graph and continue the trace in the partial implication graph, we find the same UIP, (¬b 3 ).

Hybrid Learned Clauses

A conflict-based learning procedure can learn clauses of arbitrary length from an analysis of the implication graph.

Therefore, some form of lazy implications becomes imperative. The authors of HDPLL [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF] proposed an efficient method for determining when an implication is guaranteed to occur on an arithmetic inequality. However, determining the actual implied value involves applying complex rules on each variable in the inequality. This can be very expensive on large inequalities.

To our knowledge, there has been no published work on efficient two-literal watching for word-level arithmetic constraints, with the exception of CAMA [START_REF] Liu | CAMA: a multivalued satisfiablity solver[END_REF]. CAMA's approach relies on enumeration of all values in a word-variable's domain. For example, an add operation, a=b+c, where a, b, and c are n bits each, leads to O(3.(2 n -1) 2 ) multi-valued clauses Other arithmetic operators require in the order of O(2 n -1) clauses. Our method uses an implicit representation of value sets, which makes it very efficient in practice.

Literal Watching

A conflict-avoiding constraint on word-level variables v i , is a disjunct of word-literals with associated ranges

W i b(v i ).
This can be represented either as an FD constraint or as a hybrid clause (defined in Section 2). A word-literal in a hybrid clause can evaluate to true, false or unknown. The containment function, contains(b 1 , b 2 ), of a range b 1 on another range b 2 is a three-valued function defined as:

contains(b 1 , b 2 ) =      false b 1 ∩ b 2 = / 0 true b 1 ⊆ b 2 unknown (b 1 ∩ b 2 = / 0) ∧ (b 1 ⊆ b 2 )
Now it is quite straight-forward to see that we can use containment checks on the ranges of word-literals for lazy implications. Note that the basic idea is similar to that in Boolean SAT [START_REF] Moskiewicz | Engineering an Efficient SAT Solver[END_REF]. However, we use a pessimistic containment check on word-literals as compared to an exact check in CAMA. FD constraints are more expressive than hybrid clauses, but evaluating FD constraints for new implications is very expensive as compared to hybrid clauses. For example, assume that a new value change has occurred on v 0 in the constraint ∑ n i=0 a i • v i ≥ rhs. We have to evaluate the relation,

a j • v j ≥ rhs -(∑ n i=0 a i • v i |i = j)
for all variables v j , excluding v 0 . This means that the number of evaluations of the FD constraint per implication can depend both on the current ranges and number of variables. On the other hand, any implication of hybrid-clauses can be done with, at worst, n -1 containment checks. This motivates learning hybrid clauses.

An example of two-literal watching on hybrid clauses is shown in Figure 5. Assume that v 4 is a 3-bit wordlevel variable with initial domain 0, 7 , and v 1 , v 2 , v 3 are Boolean variables. Also, assume that the set of variable assignments, {v 4 , v 1 , v 2 , v 3 } → { 3, 4 , 1, 0, 0} causes a conflict. The conflict-avoiding hybrid-clause is (¬v 1 ∨ v 2 ∨ v 3 ∨ ¬v 4 3, 4 ). It is simpler to check inclusion than exclusion of ranges for the containment check. Therefore negative literals are split into a disjunct of word-literals i.e., ¬v 4 3, 4 ≡ v 4 0, 2 ∨ v 4 5, 7 . The final learned clause, shown in Figure 5, is (¬v

1 ∨ v 2 ∨ v 3 ∨ v 4 0, 2 ∨ v 4 5, 7 ).

Implication

Watch pointers pointer move

Unknown Literal

False Literal True Literal [-,-] [-,-] [-,-] [ ) is false. The pointer on each watched literal moves to the right and left respectively. Next, assume that the value changes v 2 = 0 and v 3 = 0 occurred at decision level 2. The pointer on the watched literal, v 2 moves to the right twice, since v 3 is also false. The two pointers meet at the literal v 4 0, 2 , implying the assignment v 4 = 0, 2 .

1 v 1 v 1 v 1 v 2 v 2 v 2 v 2 v 3 v 3 v 3 v 3 v 4 v 4 v 4 v 4 v 4 v 4 v 4 v 4 v 1 v 4 v 2 v 3 v 4 v i v i v i v [-,-] [-,-] [-,-] [0,2] [5,7] [-,-] [-,-] [-,-] [0,2] [5,7] [-,-] [-,-] [-,-] [0,2] [5,7]

Experimental Analysis

In this section, we discuss some experiments on the hybrid DPLL solver. The results of the comparison experiments are shown in the scatter plots in Figures 6 and7. The x and y axis represent log 10 run-times of each tool in CPU seconds. Points above (below) the diagonal correspond to examples where the tool on the x (y) axis is faster than the other. Each division above (below) the diagonal represents an order of magnitude speed-up (slow-down) for the x tool. Points on the right (top) grid line marked Tout, indicates the x (y) system timed-out at 1200 CPU seconds. Fail, indicates the x (y) system failed with a system error (seg-fault, etc).

Comparison with Heuristic Learning

In this experiment, we compare the new techniques with the heuristic conflict analysis in [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF] on the same benchmarks in that paper. The results of this experiment are shown in the Figure 6. HDPLL old is HDPLL with the heuristic conflictbased learning in [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF]. HDPLL new is HDPLL with the new UIP-based learning. Figure 6 shows that hybrid UIP learning is faster than the method in [START_REF] Parthasarathy | An Efficient Finite-domain Constraint Solver for RTL Circuits[END_REF] by an order of magnitude on most cases. It completes on all cases where the old method aborts, in under 100 CPU seconds. Clearly, UIP learning in the combined implication-resolution graph is an efficient technique to prune the search space in HDPLL.

Comparison with state-of-the-art CDPs

We considered several tools that combine multiple decision theories including Boolean logic and some form of integer linear arithmetic for comparison with HDPLL: 1. CVC-Lite [START_REF] Stump | CVC: A Cooperating Validity Checker[END_REF] does not have a complete integer decision procedure. We used a real relaxation of the integer benchmarks only for CVC-Lite. Therefore, the results on SAT cases are reported as failures for CVC-Lite. We used CVC-Lite with the options -+sat fast. 2. Integrated Canonizer and Solver(ICS) [START_REF] Filliâtre | ICS: Integrated Canonization and Solving[END_REF] combined linear real arithmetic, bit-vectors, uninterpreted functions, and other theories. We used the default options for ICS. 3. UCLID [START_REF] Seshia | Hybrid Sat-based Decision Procedure for Separation Logic with Uninterpreted Functions[END_REF] cannot handle general arithmetic. However, we ran it on a limited set of benchmarks with counter arithmetic. We used the optionssat 0 chaff.

All the comparison CDPS timed-out on most of the properties in the old-benchmark set. Therefore, we created new benchmarks for this experiment. Our benchmarks are 35 BMC models of safety properties on the RTL circuits, shown in Table 1.

The number of properties per circuit is shown in Column 3. The maximum bound is shown in Column 4. As we can see from Figures 7(a), 7(b) and 7(c), the hybrid UIP learning techniques in HDPLL new outperforms ICS, and UCLID on almost all cases, sometimes by several orders of magnitude. CVC-Lite performed best among the compared CDPS (Figure 7(a)), with an average of 70.12 CPU seconds per property and timed-out on only two cases. However, this is due to the real relaxation, which leads to false positives.

On comparing the CDP's with a complete integer decision procedure, we see that UCLID timed-out on 3 test-cases and took an average of 199.

Asymptotic Run-time comparisons

We ran a controlled experiment to compare the asymptotic run-time growth of HPDLL versus the other CDPs. We selected a safety property on the largest circuit Met, and The results of this experiment is shown in Figure 8. The x-axis shows the length of the bound and the y-axis shows the run-time in CPU seconds. As we can see the asymptotic run-time growth of HDPLL is significantly lower than that of all the other tools. CVC-Lite performed next best with a controlled growth similar to HDPLL. It is interesting that the integer decision procedures in HDPLL can compare well with a real relaxation of the problem. UCLID and ICS showed a sharp increase in run-time after bound k =21 and k =9 respectively. The results clearly show that the asymptotic run-time of HDPLL is considerably better than these tools.

Conclusions

We presented an efficient learning scheme for a DPLLbased constraint solver for RTL circuits. We also described compact data-structures for representing these learned relations that enable efficient constraint propagation. We demonstrated experimentally that these techniques make HDPLL more efficient than current state-of-the-art CDPs. A DPLLstyle combination of decision theories seems to out-perform the other CDPs when efficient constraint propagation and conflict-based learning is used to prune the search space. In future, we shall extend the solver to other theories to handle arbitrary RTL circuits.

Figure 2 .Figure 3 .

 23 Figure 2. Hybrid DPLL algorithm.

Figure 4 .

 4 Figure 4. FME Resolution Graph on Figure 3(a).

Figure 5 .

 5 Figure 5. Hybrid clause two-literal watching Figure 5 also shows an example of two-literal watching on a hybrid learned clause. Assume that the value changes, v 1 = 1 and v 4 = 0, 4 occurred at decision level 1. The literal ¬v 1 becomes false. The word-literal v 4 5, 7 becomes false since contains( 0, 4 , 5, 7 ) is false. The pointer on each watched literal moves to the right and left respectively. Next, assume that the value changes v 2 = 0 and v 3 = 0 occurred at decision level 2. The pointer on the watched literal, v 2 moves to the right twice, since v 3 is also false. The two pointers meet at the literal v 4 0, 2 , implying the assignment v 4 = 0, 2 .

Figure 6 .

 6 Figure 6. Hybrid UIP learning v/s Heuristic [7]

  5 CPU seconds per property (Figure 7(b)). ICS timed-out on 16 out of 35 test-cases and took an average of 535.99 CPU seconds per property (Figure 7(c)). HDPLL finished all test-cases in less than 15 seconds.

Figure 7 .Figure 8 .

 78 Figure 7. Comparison of HDPLL new with CVC-Lite, ICS, and UCLID. compared the run-time growth as the bound is increased for bounded model checking. The comparisons are accurate since the complexity of each instance increases linearly.

Table 1 . Test-Case characteristics

 1

	Ckt	Description of Circuit	# Props Max. Bound
	ser	compares serial data	1	20
	BCD BCD decoder	1	20
	MM	min-max computation	1	20
	Met	digital sensor interface	9	30

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE