Brice Goglin

NIC-assisted cache-efficient receive stack for message passing over Ethernet

Keywords: High-speed networking, Cache, MPI, Ethernet, Multiqueue, Binding cpeauth.cls

High-speed networking in clusters usually relies on advanced hardware features in the NICs, such as zero-copy capability. Open-MX is a high-performance message passing stack tailored for regular Ethernet hardware without such capabilities. We present the addition of a multiqueue support in the Open-MX receive stack so that all incoming packets for the same process are handled on the same core. We then introduce the idea of binding the target end process near its dedicated receive queue. This model leads to a more cache-efficient receive stack for Open-MX. It also proves that very simple and stateless hardware features may have a significant impact on message passing performance over Ethernet. The implementation of this model in a firmware reveals that it may not be as efficient as some manually tuned micro-benchmarks. But our multiqueue receive stack generally performs better than the original single queue stack, especially on large communication patterns where multiple processes are involved and manual binding is difficult.

INTRODUCTION

The emergence of 10-gigabit/s Ethernet hardware raised the questions of when and how the long-awaited convergence with high-speed networks will become a reality. Ethernet now appears as an interesting networking layer within local area networks for various protocols such as FCoE [START_REF]FCoE (Fibre Channel over Ethernet[END_REF]. Meanwhile, several network vendors that previously focused on highperformance computing added interoperability with Ethernet to their hardware, such as Mellanox ConnectX [START_REF]Mellanox ConnectX -4th Generation Server & Storage Adapter Architecture[END_REF] or Myricom Myri-10G [START_REF]Myricom Myri-10G[END_REF]. However, these technologies still require dedicated interfaces in the nodes. The gap between these advanced NICs and regular Ethernet NICs remains substantial. It brings the question of which hardware feature will become legacy once the actual convergence will be reached.

Several research works were carried out in the context of high-performance message passing over Ethernet as a way to improve the overall parallel computing performance without requiring expensive networking hardware. GAMMA [START_REF] Ciaccio | GAMMA and MPI/GAMMA on gigabitethernet[END_REF] or EMP [START_REF] Shivam | EMP: Zero-copy OS-bypass NIC-driven Gigabit Ethernet Message Passing[END_REF] only work on a limited spectrum of hardware since they use modified drivers or hardware. Our Open-MX [START_REF] Goglin | Design and Implementation of Open-MX: High-Performance Message Passing over generic Ethernet hardware[END_REF] stack is another message passing model implemented on top of the Ethernet software layer of the Linux kernel. It offers high-performance communication over any generic Ethernet hardware using the wire specifications and the application programming interface of Myrinet Express [START_REF] Myricom | Myrinet Express (MX): A High Performance, Low-Level, Message-Passing Interface for Myrinet[END_REF]. However, like QMP [START_REF] Chen | Message Passing for Linux Clusters with Gigabit Ethernet Mesh Connections[END_REF] and PM [START_REF] Sumimoto | A Scalable Communication Layer for Multi-Dimensional Hyper Crossbar Network Using Multiple Gigabit Ethernet[END_REF] (or any other software-based message passing), being compatible with any legacy Ethernet NICs also means that Open-MX suffers from limited hardware features. For instance, it has to work around the inability to perform zero-copy receive by offloading memory copy on Intel I/O Acceleration Technology (I/OAT) [START_REF] Goglin | Improving Message Passing over Ethernet with I/OAT Copy Offload in Open-MX[END_REF].

We propose to improve the cache-efficiency of the receive side of Ethernet-based message passing by extending the hardware IP multiqueue support to filter Open-MX packets as well. Such a stateless feature requires very little computing power and software support compared to the existing complex and stateful features such as zero-copy or TOE (TCP Offload Engine). Parallelizing the stack is known to be important on modern machines [START_REF] Willmann | An Evaluation of Network Stack Parallelization Strategies in Modern Operating Systems[END_REF]. We are looking at it in the context of binding the whole packet processing to the same core, from the bottom interrupt handler up to the application.

This paper is an extended revision of [START_REF] Goglin | NIC-assisted Cache-Efficient Receive Stack for Message Passing over Ethernet[END_REF] organized as follows. We present Open-MX, its possible cache-inefficiency problems, related works and our motivations in Section 2. Section 3 describes our proposal to combine the multiqueue extension in the Myri-10G firmware and its corresponding support in Open-MX so as to we build an automatic binding facility for both the receive handler in the driver and the target application. Section 4 presents a performance evaluation which shows that our model achieves satisfying performance for microbenchmarks, reduces the overall cache miss rate, and improves performance in the case of large communication patterns.

BACKGROUND AND MOTIVATIONS

In this section, we briefly describe the Open-MX stack and how the cache is involved on the receive side. We then present previous works on the cache efficiency of high-performance networking stacks. We finally detail our motivation to add some Open-MX specific support in the NIC and our objectives with this implementation.

Cache Efficiency Issues in the Open-MX Stack

The Open-MX stack * aims at providing high-performance message passing over any generic Ethernet hardware. First, it bypasses the usual TCP/IP stack so as to exploit the networking hardware directly without suffering from the overhead of features that are not that useful in clusters, such as congestion control. It then exposes the Myrinet Express API (MX) [START_REF] Myricom | Myrinet Express (MX): A High Performance, Low-Level, Message-Passing Interface for Myrinet[END_REF] to user-space applications so that many existing middleware projects such as Open MPI [START_REF] Gabriel | Open MPI: Goals, concept, and design of a next generation MPI implementation[END_REF] or PVFS2 [START_REF]The Parallel Virtual File System[END_REF] run successfully unmodified on top of it. Open-MX is also interoperable with hosts running the native MX stack over Ethernet (MXoE). This wire compatibility is a key feature of Open-MX. It is under experimentation at Argonne National Laboratory to provide a PVFS2 transport layer between BlueGene/P compute and storage nodes. The compute nodes running Open-MX are connected through a Broadcom 10-gigabit Ethernet interface to storage nodes with a Myri-10G interface running the native MXoE stack.

To achieve these goals, Open-MX was first designed as an emulated MX firmware in a Linux kernel module [START_REF] Goglin | Design and Implementation of Open-MX: High-Performance Message Passing over generic Ethernet hardware[END_REF]. This way, legacy applications built for MX benefit from the same abilities without needing the Myricom hardware or the native MX software stack (see Figure 1). However, the features that are usually implemented in the hardware of high-speed networks are obviously prone to performance issues when emulated in software. Indeed, portability to any Ethernet hardware requires the use of a common very simple low-level programming interface to access drivers and NICs.

The inability of generic NICs to implement advanced mechanims such as zero-copy data transfer leads to many possible cache efficiency issues. Reducing cache effects in the Open-MX stack requires to ensure that data structures are not used concurrently by multiple cores. Since the send side is mostly driven by the application, the whole send stack is executed by the same core. The receive side is however much more complex. As any other Ethernet-based receive stack, Open-MX processes incoming packets in its Receive handler which is invoked when the Ethernet NIC raises an interrupt. The receive handler first acquires the descriptor of the communication channel (endpoint). Then, if the packet is part of a eager message (i.e. ≤ 32 kB), the data and corresponding event are written into a ring shared with the user-space library. Finally, the library will copy the data back to the application buffers (see Figure 2).

If the packet is part of a large message (after a rendezvous), the corresponding Pull handle is acquired and updated. Then, the data is copied into the associated receive buffer (Figure 2). An event is raised at the user-space level only when the last packet is received. This copy may be offloaded to Intel I/O Acceleration Technology (I/OAT) DMA engine hardware if available [START_REF] Goglin | Improving Message Passing over Ethernet with I/OAT Copy Offload in Open-MX[END_REF]. The current Open-MX receive stack will most of the times receive IRQ (Interrupt ReQuest) from all cores since the hardware chipset usually distributes them in a round-robin manner (as depicted by Figure 3(a) later). Having different cores access shared resources causes cache-lines bounces between these cores. It explains why processing all packets for the same endpoint on the same core will improve the cache-efficiency: Having a single core access the endpoint structure or shared ring in the driver leads to no more cache-line bounces and no more concurrent accesses to these shared resources. Additionally, all eager packets will also benefit from having the user-space library run on the same core since a shared ring is involved.

Copy event+data

Copy data Update

Endpoint

Large messages (Pull packets) will also benefit from having their handles accessed by a single core. This is actually guaranteed by the fact that each handle is used by a single endpoint. Moreover, running the application on the same core will reduce cache effects when accessing the received data (except if the copy was offloaded to the I/OAT hardware which bypasses the cache).

In the end, all incoming Open-MX packets have to be processed in the operating system on any of the cores and then passed to user-space where the application probably runs on another core. Cache efficiency thus suffers from concurrent accesses in the operating system and between the driver and the user-space application.

Related Works

Proper use of caches may have a critical impact on performance. Many research works have been carried out to improve cache efficiency of high performance computing, from cache oblivious algorithms [START_REF] Frigo | Cache-Oblivious Algorithms[END_REF] up to low-level hardware improvements. Networking communications are also subject to cache efficiency problems as explained in the previous section, but the actual issues highly depend on the hardware features and software implementation.

High-performance communication in clusters heavily relies on specific features provided by the networking hardware, such as Mellanox ConnectX [START_REF]Mellanox ConnectX -4th Generation Server & Storage Adapter Architecture[END_REF] or Myricom Myri-10G [START_REF]Myricom Myri-10G[END_REF]. The most famous hardware feature for HPC remains zero-copy support. It has also been added to some Ethernet-based message passing stacks, for instance by relying on RDMA-enabled hardware and drivers, such as EMP [START_REF] Shivam | EMP: Zero-copy OS-bypass NIC-driven Gigabit Ethernet Message Passing[END_REF] or recently iWarp [START_REF] Rashti | 10-Gigabit iWARP Ethernet: Comparative Performance Analysis with Infiniband and Myrinet-10G[END_REF]. This strategy achieves a high throughput for large messages. But it requires complex modifications of the operating system (since the application must be able to provide receive buffers to the NIC) and of the NIC (which decides which buffer should be used when a new packet arrives). High-speed networks do not suffer from many cache-related problems since events and data are directly deposited in the user-space application context without any intermediate cache-polluting copy. Regular Ethernet hardware do not benefit from such a model, it only offers an interrupt-driven model. The host operating system processes incoming packets only when the NIC raises an interrupt. It then passes them to the user-space application. This mechanism prevents applications from directly polling the NIC for incoming packets. And it implies cache-line bounces unless the operating system stack and application are carefully bound to the same processor.

Several research projects specifically did target high-performance message passing over Ethernet in the past. The most popular one is GAMMA [START_REF] Ciaccio | GAMMA and MPI/GAMMA on gigabitethernet[END_REF] which only works on a limited hardware range since it uses a modified driver which does not support regular TCP/IP anymore. MultiEdge [START_REF] Karlsson | MultiEdge: An Edge-based Communication Subsystem for Scalable Commodity Servers[END_REF] uses a similar design on recent 1-and 10-gigabit hardware and thus achieves good bandwidth, but yields quite high latency levels. EMP [START_REF] Shivam | EMP: Zero-copy OS-bypass NIC-driven Gigabit Ethernet Message Passing[END_REF] goes even further by modifying the firmware of some programmable boards to achieve better performance. Such software or hardware modifications may reduce cache-efficiency issues thanks to reduced memory copy requirements or application-directed polling. However, such implementations do not support regular hardware and software stacks. Open-MX relies on the generic Ethernet layer of Linux and thus may use any hardware. It may also coexist with the TCP/IP stack that is still often used for administration or storage purposes. MPI/QMP [START_REF] Chen | Message Passing for Linux Clusters with Gigabit Ethernet Mesh Connections[END_REF] uses a Open-MX-like model, based on M-VIA, to achieve large bandwidth over multiple regular Ethernet links. PM/Ethernet-HXB [START_REF] Sumimoto | A Scalable Communication Layer for Multi-Dimensional Hyper Crossbar Network Using Multiple Gigabit Ethernet[END_REF] offers a similar design and supports trunked Ethernet connections. They both achieve interesting performance levels thanks to multiple underlying Ethernet connections, but are not designed for single high-performance connections such as Myri-10G. Open-MX is designed to efficiently use modern Ethernet hardware. It does require the aggregation of multiple links to achieve highperformance, but it may also transparently use a trunked connection to aggregate multiple links if desired. However, in the end, all these software implementations suffer from similar cache problems due to similar paths for events and data from the NIC up to the application: The operating system processes packets on different cores and then passes them to the application running on likely yet another core.

An interesting way to avoid cache-polluting memory copies is to use virtual memory tricks to remap the source buffer in the target virtual address space. Such a strategy has been studied for a long time to offer zero-copy socket implementations [START_REF] Jerry | Zero-Copy TCP in Solaris[END_REF] and more recently for Ethernetbased message passing [START_REF] Passas | Towards 100 Gbit/s Ethernet: Multicore-based Parallel Communication Protocol Design[END_REF]. However, even if memory copies are avoided, cache pressure remains high since remapping requires cache flushing. Also, careful binding of the operating system stack and of the application is still required so as to avoid cacheline bounces between the processing components along the receive stack. Moreover, this strategy has multiple cornercases caused by modern operating systems heavily relying on multiple page states, pages being shared, miss-alignment, or memory pinning. It makes remapping technically difficult and expensive in many cases while this idea was indeed very interesting for performance and CPU load reduction purposes. Some Ethernet-specific hardware optimizations have been developed in the context of IP networks, but they were not designed for HPC. Advanced NICs now enable the offload of TCP fragmentation/re-assembly (TSO and LRO) to decrease the packet rate in the host [START_REF] Grossman | Large Receive Offload Implementation in Neterion 10GbE Ethernet Driver[END_REF]. But this work does not apply to message-based protocols such as Open-MX and does not improve cache efficiency. Another famous recent innovation is multiqueue support [START_REF] Yi | Enabling Linux Network Support of Hardware Multiqueue Devices[END_REF]. This packet filtering facility in the NIC enables interesting receive performance improvement for IP thanks to a better understanding of the location of the receive stack in the host. We look further at this idea in the following sections.

Proposal

The cache-efficiency of the receive stack is significantly related to the actual hardware and software implementation since features such as zero-copy and application-directed polling reduce cache utilization. However, all message passing stacks implemented on top of the generic Ethernet layer such as Open-MX suffer from similar cache issues since packets are processed in the driver on any core (with possible concurrent accesses) and then passed to the user-space application that likely runs on another core. We propose a study of this problem in the context of Open-MX.

A simple way to avoid concurrent accesses in the driver is to bind the interrupt to a single core. However, the chosen core will be overloaded, causing an availability imbalance between cores. Moreover, all processes running on other cores will suffer from cache-line bounces in their shared ring since they would compete with the chosen core. In the end, this solution may only be interesting for benchmarking purposes with a single process per node (see Section 4).

As explained above, the study of cache-efficiency in the context of TCP/IP led to the emergence of hardware multiqueue support. Several modern NICs have the ability to split the incoming packet flow into several queues [START_REF] Yi | Enabling Linux Network Support of Hardware Multiqueue Devices[END_REF] with different interrupts. By filtering packets depending on their IP connection and binding each queue to a single core, it is possible to ensure that all packets of a connection will be processed by the same core. It prevents many cache-line bounces in the host receive stack.

We propose in this article to study the addition of Open-MX-aware multiqueue support. Such a feature is becoming widely available in recent 1-or 10-gigabit NICs. We expect to improve the cache-efficiency of our receive stack by guarantying that all packets going to the same endpoint are processed on the same core. To improve performance even further, we then propose to bind the target user-process to the core where the endpoint queue is processed. It will make the whole Open-MX receive stack much more cache-friendly. This idea goes further than existing IP implementations where the cache-efficiency property is not transferred to the application.

The intent of this work is also to demonstrate that very simple hardware features may bring interesting performance improvements. While complex hardware features have been proposed to improve networking in HPC (for instance zero-copy or application polling support), our hardware modifications are very simple and should be applicable to many legacy NICs. The Open-MX specific support will be Stateless and based on existing multiqueue support, with a new dedicated packet filtering strategy.

DESIGN OF A CACHE-FRIENDLY OPEN-MX RECEIVE STACK

We now detail our design and implementation of a cache-friendly receive stack in Open-MX thanks to the addition of dedicated multiqueue support in the NIC and the corresponding user process binding facility.

Open-MX-aware Multiqueue Ethernet support

Hardware multiqueue support is based on the driver allocating one MSI-X interrupt vector (similar to an IRQ line) and one ring per receive queue. Then, for each incoming packet, the NIC decides which receive queue should be used [START_REF] Yi | Enabling Linux Network Support of Hardware Multiqueue Devices[END_REF]. The IP traffic is dispatched into multiple queues by hashing each connection into a queue index. This idea improves performance by having multiple packets from the same connection be processed together, thus improving locality.

The Open-MX multiqueue support is actually very simple because hashing its packets is easy. Indeed, the same communication channel (endpoint) is used to communicate with many peers, so only the local endpoint identifier has to be hashed. Therefore, the NIC only has to convert the 8-bit destination endpoint identifier into a queue index. Considering the slowness of NIC processors, this conversion is much more simple than hashing IP traffic where many connection parameters (source and destination, port and address) have to be involved in the hash function. This model is summarized in Figure 3(b).

All packets for the same destination endpoint are now placed in the same receive queue, the processing of each endpoint channels may be dispatched to different cores. The next step towards a cache-friendly receive stack is to bind each process to the core which handles the receive queue of its endpoint.

Multiqueue-aware Process Binding

Now that the receive handler is guaranteed to always run on the same core for all packets of the same endpoint, we discuss how to have the application run there as well. One solution would be to move the receive queue near the target process when it actually opens the corresponding endpoint. However, moving receive queues depending on process placement may easily break their load-balance, causing multiqueueIP performance to decrease. Since Open-MX was designed to coexist with the IP stack, the binding of all queues has to remain managed globally and independently of the process placement.

We have chosen the opposite solution: keep receive queues bound as usual (one queue per core) and make Open-MX applications migrate on the right core. Therefore, when an application opens an endpoint, the Open-MX library will bind it near the corresponding receive queue as depicted on Figure 3(b) and explained in the next section. Since most high-performance computing applications place one process per core, and since most MPI implementations use a single endpoint per process, we expect each core to be used by a single endpoint. In the end, each receive queue will actually be used by a single endpoint as well. It makes the whole model very simple. Additionally, this model enables the pre-warming of processor caches with incoming packets thanks to Intel Direct Cache Access [START_REF] Huggahalli | Direct Cache Access for High Bandwidth Network I/O[END_REF]. This strategy would further improve performance by avoiding cache misses when the receive handler starts processing a new packet, but we did not have any DCA-enabled machine to test it.

Implementation

We implemented this model in the Open-MX stack with Myricom Myri-10G NICs as an experimentation hardware. We have chosen this board because it was one of the very first NICs with multiqueue receive support. It also enables comparisons with the MX stack which may run on the same hardware (with a different firmware and software stack that was designed for MPI).

We implemented the proposed modification in the myri10ge firmware by adding our specific packet hashing. It decodes native Open-MX packet headers to find out the destination endpoint number as specified in the MX wire specifications. Once the Ethernet driver has been setup with one receive queue per core as usual, each endpoint packet flow is sent to a single core.

Meanwhile, we added to the myri10ge driver a routine that returns the MSI-X interrupt vector that will be used for each Open-MX endpoint. When Open-MX attaches an interface whose driver exports such a routine, it gathers all interrupt affinities (the binding of the receive queues). Then, it provides the Open-MX user-space library with binding hints when it opens an endpoint. Applications are thus automatically migrated onto the core that will process their packets. It makes the whole stack more cache-friendly, as described on Figure 3(b).

PERFORMANCE EVALUATION

We now present a performance evaluation of our model. After describing our experimentation platform, we will detail micro-benchmarks and application-level performance.

Experimentation Platform

Our experimentation platform is composed of 2 machines with 2 Intel Xeon E5345 quad-core Clovertown processors (2.33 GHz). These processors are based on 2 dual-core sub-chips with a shared L2 cache as described in Figure 4. It implies 4 possible process/interrupt bindings : on the same core (SC), on a core sharing a cache (S$), on another core of the same processor (SP), and on another processor (OP).

These machines are connected with Myri-10G interfaces running in Ethernet mode with our modified myri10ge firmware and driver. We use Open MPI 1.2.6 [START_REF] Gabriel | Open MPI: Goals, concept, and design of a next generation MPI implementation[END_REF] on top of Open-MX 0.9.2 with Linux kernel 2.6.26. The MPI ping-pong latency on this setup is close to 10 µs (8 µs with a native Open-MX ping-pong). It may also achieve 9 out the raw 10-gigabit/s line-rate when enabling I/OAT copy offload [START_REF] Goglin | Improving Message Passing over Ethernet with I/OAT Copy Offload in Open-MX[END_REF].

Impact of Binding on Micro-Benchmarks

Table I presents the latency and throughput of Intel MPI Benchmark [START_REF]Intel MPI Benchmarks[END_REF] Pingpong depending on the process and interrupt binding. Three key results have to be noticed. First, it shows that the original model (with a single interrupt dispatched to all cores in a roundrobin manner) is slower than any other model, due to cache-line bounces. Indeed, consecutive packets are never processed by the same core in the operating system. So the endpoint and pull handle descriptors keep moving from one cache to another. Additionally, the user-space application is running on a single core, so seven out of eight packets on average have to move from one cache to another when being delivered to user-space by the driver.

Secondly, when binding the single interrupt to a single core, the best performance is achieved when the process and interrupt handler share a cache but do not actually use the same core. Indeed, this case reduces the overall latency thanks to cache hits in the receive stack, while it prevents the user-space library and interrupt handler from competing for the same core. This configuration is optimal when benchmarking a single process per node but obviously is not applicable to real applications with one process per core. Thirdly, multiqueue support achieves satisfying performance, but remains a bit slower than optimally bound single interrupt. It is related to the multiqueue implementation requiring more work in the NIC than the single interrupt firmware. This overhead is actually related to the generic multiqueue support in the firmware. Our Open-MX specific additions only bring a dozen lines of code and two logical tests. While being a bit slower than optimally bound single interrupt, this model however works with multiple processes per node, which is what real application actually require.

Idle Core Avoidance

The above results assumed that one process was running on each core even if only two of them were actually involved in the MPI communication. This setup has the advantage of keeping all cores busy. However, it may be far from the behavior of real applications where for instance disk I/O may put some processes to sleep and cause some cores to become idle. If an interrupt is raised onto such an idle core, it will likely be asleep because of power saving, and will thus have to wakeup before processing the packet. On modern processors, this wakeup overhead is several microseconds, causing the overall latency to increase significantly.

To study this problem, we ran the previous experiment with only one communicating process per node, which means 7 out of 8 cores are idle (they were busy waiting in a MPI barrier during the previous experiment). When interrupts are not bound to the right core † , it increases the latency from 11 up to 15-20 µs and reduces the throughput by roughly 20 %. This result is another justification of our idea to bind the process to the core that runs its receive queue. Indeed, if a MPI application is waiting for a message, the MPI implementation will usually busy poll the network. Its core will thus not enter any sleeping state. By binding the receive queue interrupt and the application to the same core, we guarantee that this busy polling core will be the one processing the incoming packet in the driver. It will be able to process it immediately, causing the observed latency to be much lower. All other cores that may be sleeping during disk I/O will not be disturbed by packet processing for unrelated endpoints. This result may even reduce the overall power consumption of the machine.

Cache Misses

Table II presents the percentage of cache misses observed with PAPI [START_REF] Browne | A Portable Programming Interface for Performance Evaluation on Modern Processors[END_REF] during a ping-pong depending on interrupt and process binding. Only L2 cache accesses are presented since the impact on L1 accesses appears to be lower, possibly because our overall workload is much larger than the 32 kB L1 caches.

The table first shows that the cache miss rate is dramatically reduced for small messages thanks to our multiqueue support. Running the receive handler (the kernel part of the stack) always on the same core divides cache misses in the kernel by 2. Binding the target application (the user part of the stack) to the same core further reduces user-space cache misses by a factor of up to 100.

Cache misses are not improved for 32 kB message communication. This behavior is caused by the number of copies that are involved on the receive path. Indeed, one drawback of the current Open-MX implementation up to 32 kB messages is the matching of MPI messages in user-space: it requires one copy from the kernel inside the shared ring and another copy back from the ring into the application destination buffer. These copies cause too many cache pollution, which prevents our cache efficiency improvements from being visible.

Very large messages with I/OAT copy offload do not involve any data copy in the receive path. Cache misses are thus mostly related to concurrent accesses to the endpoint and pull handles in the driver. We observe a slightly decreased cache miss rate thanks to proper binding. But the overall rate remains high, likely because it involves some code-paths outside of the Open-MX receive stack (rendezvous handshake in user-space, send stack, ...) which are expensive for large messages.

Collective Communication

After demonstrating that our design improves cache-efficiency without strongly disturbing micro-benchmark performance, we now focus on complex communication patterns by first looking at collective operations. We ran IMB Alltoall between our nodes with one process per core. Figure 5 presents the execution time compared to the native MX stack, depending on interrupt and receive queue binding. It shows that using a single receive queue results in worse performance than our multiqueue support. As expected, binding this single interrupt to a single core decreases the performance as soon as the message size increases since the load on this core becomes the limiting factor. When multiqueue support is enabled, the overall Alltoall performance is on average 1.3 better. It now reaches less than 150 % of the native MX stack execution time for very large messages when I/OAT copy offload is enabled. Moreover, our implementation is even able to outperform MX near 4 kB message sizes ‡ . This result reveals that our implementation achieves its biggest improvement when the communication pattern becomes larger and more complex (collective operation with many local processes). We think it is caused by such patterns requiring more data transfer within the host and thus making cache-efficiency more important. [START_REF] Bailey | The NAS Parallel Benchmarks[END_REF] between our two 8-core hosts. Most programs show a few percents performance improvement thanks to our work. This impact is limited by the fact that these applications are not highly communication intensive. IS (which performs many large message communications) shows an impressive speedup (8.5 for class B, 2.6 for class C). Thanks to our multiqueue support, IS is now even faster on Open-MX than on MX. We feel that such a huge speedup cannot be only related to the efficiency of our new implementation. It is likely also caused by poor performance of the initial single-queue model because of very poor cache efficiency Indeed, looking at cache miss rates confirms that they are dramatically reduced by our multiqueue implementation, by a factor of about 11 on IS. It is again worth noticing that using a single interrupt bound to a single core sometimes decreases performance. As explained earlier, this configuration should only be preferred for micro-benchmarking with very few processes per node.

CONCLUSION AND PERSPECTIVES

While HPC networking relies on complex hardware features such as zero-copy, Ethernet remains simple. The Open-MX message passing stack achieves interesting performance on top of it without benefiting from advanced features in the networking hardware. This paper presents a study of the cache-efficiency of the Open-MX receive stack.

We looked at the binding of interrupt processing in the driver and of the library in user-space. We proposed the extension of the existing IP hardware multiqueue support which assigns a single core to each connection. It prevents shared data structures from being concurrently accessed by multiple cores. Open-MX specific packet hashing has been added into the official firmware of Myri-10G boards § so as to associate a single receive queue with each communication channel. Secondly, we further extended the model by enabling the automatic binding of the target end application to the same core. Therefore, there are fewer cache-line bounces between cores from the interrupt handler up to the target application.

Performance evaluations first shows that the usual single-interrupt based model may achieve very good performance when using a single task and binding it so that it shares a cache with the interrupt handler. However, as soon as multiple processes and complex communication patterns are involved, the performance of this model suffers, especially from load imbalance between the cores. Using a single-interrupt scattered to all cores in a round-robin manner distributes the load but it shows limited performance due to many cache misses.

Our proposed multiqueue implementation distributes the load as well. It also offers satisfying performance for simple benchmarks. Moreover, binding the application near its receive queue further improves the overall performance thanks to fewer cache misses occurring on the receive path and thanks to the target core being ready to process incoming packets. Communication intensive patterns reveal a large improvement since the impact of cache pollution is larger when all cores and caches are busy. Open-MX is now even able to perform faster than the native MX stack in some cases. We observe more than 30 % of improvement for Alltoall operations, while the execution time of the communication intensive NAS parallel benchmark IS is reduced by a factor of up to 8.

These results demonstrate that very simple hardware features enable significant performance improvement. Indeed, multiqueue support is becoming a standard feature that many NIC now implement. Our implementation is Stateless and does not require any intrusive modification of the NIC or host, contrary to usual HPC innovations. Such features that can be easily implemented in legacy NICs, open a large room for improvement of message passing over Ethernet networks.

Figure 1 .

 1 Figure 1. Design of the native MX and generic Open-MX software stacks.

Figure 2 .

 2 Figure 2. Resource accesses and data transfers along the Open-MX receive stack.

  Round-Robin Single-Interrupt: the interrupt goes to any core while the application may run somewhere else. Open-MX-aware Multiqueue: the NIC raises the MSI-X interrupt corresponding to the core where the application runs.

Figure 3 .

 3 Figure 3. Path from the NIC interrupt up to the application receiving the event and data.

Figure 4 .

 4 Figure 4. Processors and caches in the experimentation platform (OS-numbered).

Figure 5 .

 5 Figure 5. IMB Alltoall relative execution time depending on interrupt binding and multiqueue support, compared with the native MX stack.

Table I .

 I IMB Pingpong performance depending on process and IRQ binding.

	Metric	Binding	SC	S$	SP	OP
		Round-Robin Single IRQ		≃ 11.4 µs
	0 byte latency	Single IRQ on core #0	10.96 9.34 10.32 10.25
		Multiqueue		10.10
		Round-Robin Single IRQ		≃ 646 MiB/s
	4 MB throughput	Single IRQ on core #0	719	723	721	714
		Multiqueue		707
		Round-Robin Single IRQ		≃ 905 MiB/s
	4 MB throughput (I/OAT)	Single IRQ on core #0	1056 1059 1048	1026
		Multiqueue		965

Table II .

 II L2 cache misses (Kernel+User) during a ping-pong.

	Length	Round-Robin IRQ	IRQ on S$	IRQ on SC
	0 B	29.80 % + 13.79 %	29.70 % + 8.34 %	11.47 % + 0.13 %
	128 B	26.80 % + 17.90 % 25.06 % + 23.05 % 14.15 % + 0.51 %
	32 kB	28.77 % + 17.71 % 23.17 % + 29.32 % 24.49 % + 22.56 %
	1 MB (I/OAT)	27.7 % + 6.28 %	36.9 % + 7.97 %	25.20 % + 5.96 %

Table III .

 III NAS Parallel Benchmark execution time and improvement.Table III presents the execution time of some NAS Parallel Benchmarks

		Single IRQ	Single IRQ	Multiqueue Performance	MX
		Round-Robin on Single core		Improvement
	cg.B.16	34.62 s	34.32 s	33.68 s	+2.8 %	32.23 s
	mg.B.16	4.14 s	4.19 s	4.02 s	+2.9 %	3.93 s
	ft.B.16	22.80 s	23.06 s	21.34 s	+6.8 %	19.61 s
	is.B.16	11.84 s	10.83 s	1.25 s	×8.5	1.33 s
	is.C.16	14.69 s	14.17 s	5.62 s	×2.6	6.30 s
	4.6. Application-level Performance

ACKNOWLEDGEMENTS

We would like to thank Hyong-Youb Kim, Andrew J. Gallatin, and Loïc Prylli from Myricom, Inc. for helping us when modifying the myri10ge firmware.


F Herbreteau

B Srivathsan

Efficient On-The-Fly Emptiness Check for Timed Büchi Automata

 for a survey). The best known algorithms in the case of multiple Büchi conditions are inspired by the Tarjan's SCC algorithm. An on-the-fly algorithm which computes the graph during the search, and terminates as soon as a satisfactory SCC is found, is crucial in the timed settings as the zone graph is often huge. It is known that the Couvreur's algorithm [9] outperforms all on-the-fly SCC-based algorithms.

In this paper, we present an on-the-fly algorithm that solves the emptiness problem for timed Büchi automata. We noticed from several experiments that Büchi emptiness can sometimes be decided directly from the zone graph, i.e. without using any extra construction. This is the way we take here. The Couvreur's algorithm is employed to search for an accepting SCC directly on the zone graph. Then, we face two challenges.

The first challenge is to detect if this SCC has blocking clocks, that is clocks that are bounded from above but are not reset in the transitions of the SCC. The SCCs with blocking clocks have to be re-explored by discarding transitions bounding these clocks. Notice that discarding edges may split the SCC into smaller SCCs. The difficult task is to discover the smaller SCCs and explore them on-the-fly.

The second challenge is to handle SCCs with zero-checks, that is clocks that are tested for value being zero. In this case, the zone graph does not contain enough information to detect time progress. This is where the guessing zone graph construction is required. The involving part of the problem is to introduce this construction on-the-fly. In particular the part of the guessing zone graph that is explored should be restricted only to the transitions from the SCC containing zero-checks.

We propose an algorithm that fulfills both challenges. In the worst case, it runs in time O(|ZG|.(|X| + 1) 2 ). When the automaton does not have zero checks it runs in time O(|ZG|.(|X| + 1)). When the automaton further has no blocking clocks, it runs in time O(|ZG|). Our algorithm further incorporates an improvement that proves powerful in practice. Indeed, non-Zenoness could be

Introduction

Timed automata [1] are finite automata extended with clocks. The clock values can be compared with constants and reset to zero on the transitions, while they evolve continuously in the states. The emptiness problem for timed automata is decidable. Consequently, timed automata are used in tools like Uppaal [3] and Kronos [START_REF] Bozga | Kronos: a mode-checking tool for real-time systems[END_REF] for model-checking reachability properties of real-time systems. They have also been successfully used for industrial case studies, e.g. [START_REF] Bérard | Analysing the pgm protocol with UPPAAL[END_REF].

For the verification of liveness properties, timed automata with Büchi conditions have been considered. The emptiness problem demands if there exists a non-Zeno run that visits an accepting state infinitely often. A run is non-Zeno if the total time elapsed during the run is unbounded. This further requirement makes the problem harder than classical Büchi emptiness.

The solution proposed in [1] relies on a symbolic semantics called the region graph. The emptiness problem for timed Büchi automata is reduced to classical Büchi emptiness on the region graph with an additional time progress requirement. However, the region graph construction is very inefficient for model checking real life systems. Zones are used instead of regions in the aforementioned tools. The zone graph is another symbolic semantics that is coarser than the region graph. Although it is precise enough to preserve reachability properties, it is too abstract to directly infer time progress and hence non-Zenoness.

Two approaches have been proposed in order to ascertain time progress. In [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF], the automaton is transformed into a so-called strongly non-Zeno automaton, which has the property that all the runs visiting an accepting state infinitely often are non-Zeno. Hence, non-Zenoness is reduced to Büchi emptiness. However it has been proved in [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF] that this construction sometimes results in an exponential blowup.

A careful look at the conditions for Zenoness yields another solution to verify time progress. Two situations can prevent time from diverging on a run. Either the value of a clock is bounded and not reset anymore, or some clock is reset and later checked to zero preventing time elapse in-between. In [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF] a guessing zone graph has been introduced to identify clear nodes where time can elapse despite zero-checks. Hence timed Büchi automata emptiness reduces to Büchi emptiness on the guessing zone graph with two infinitary conditions namely clear nodes and accepting nodes. The guessing zone graph is only |X| + 1 times bigger than the zone graph, where |X| stands for the number of clocks. The straightforward algorithm handling both the above mentioned situations explores the guessing zone graph O(|X|) number of times.

established from situations where the value of some clock is known to increase by 1 infinitely often. Even in the presence of zero-checks, this property avoids exploring the guessing zone graph. Again, this improvement is applied on-the-fly.

Next, we show that all these operations on SCCs can be handled efficiently as the memory needed by our algorithm is comparable to the memory usage of the strongly non-Zeno approach in [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF].

Finally, we also report some successful experiments of our algorithm on examples from the literature. All the experiments that we have conducted show that non-Zenoness constructions need not be applied mechanically, hence validating our approach.

Related work. Timed automata with Büchi conditions have been introduced in the seminal paper [1]. The zone approach to model-checking has been introduced in [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF] and later used in the context of timed automata [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. The Büchi emptiness problem using zones has been studied in [START_REF] Bouajjani | On-the-fly symbolic model checking for real-time systems[END_REF][START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF][START_REF] Tripakis | Checking timed büchi emptiness on simulation graphs[END_REF]. The idea of the strongly non-Zeno approach first appears in [START_REF] Tripakis | Verifying progress in timed systems[END_REF]. The strongly non-Zeno construction has been implemented in the tool Profounder [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF]. Finally, the recent paper [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF] introduces the guessing zone graph construction.

Outline. The paper is organized as follows. In Section 2 we define the emptiness problem. Then we present the two approaches that ensure time progress in Section 3. We detail our algorithm and its optimizations in Section 4. Finally, we discuss experiments and future work in Section 5.

The Emptiness Problem for Timed Büchi Automata

Timed Büchi Automata

Let X be a set of clocks, i.e., variables that range over R ≥0 , the set of nonnegative real numbers. Clock constraints are conjunctions of comparisons of variables with integer constants, e.g. (x ≤ 3 ∧ y > 0). Let Φ(X) denote the set of clock constraints over clock variables X.

A clock valuation over X is a function ν : X → R ≥0 . We denote R X ≥0 the set of clock valuations over X, and 0 : X → {0} the valuation that associates 0 to every clock in X. We write ν |= φ when ν satisfies φ, i.e. when every constraint in φ holds after replacing every x by ν(x).

For a valuation ν and δ ∈ R ≥0 , let (ν + δ) be the valuation such that (ν +

δ)(x) = ν(x) + δ for all x ∈ X. For a set R ⊆ X, let [R]ν be the valuation such that ([R]ν)(x) = 0 if x ∈ R and ([R]ν)(x) = ν(x) otherwise. A Timed Büchi Automaton (TBA) is a tuple A = (Q, q 0 , X, T, Acc) where Q is a finite set of states, q 0 ∈ Q is the initial state, X is a finite set of clocks, Acc ⊆ Q is a set of accepting states, and T ⊆ Q × Φ(X) × 2 X × Q is a finite set of transitions (q, g, R, q ′ )
where g is a guard, and R is a reset of the transition. Examples of TBA are depicted in Figure 1.

A configuration of A is a pair (q, ν) ∈ Q × R X ≥0 ; with (q 0 , 0) being the initial configuration. A discrete transition between configurations (q, ν) t ⇀ (q ′ , ν ′ ) for t = (q, g, R, q ′ ) is defined when ν g and ν ′ = [R]ν. We also have delay transitions between configurations: (q, ν) δ ⇁ (q, ν + δ) for every q, ν and δ ∈ R ≥0 . We write (q, ν)

δ,t -→ (q ′ , ν ′ ) if (q, ν) δ ⇁ (q, ν + δ) t ⇀ (q ′ , ν ′ ).
A run of A is a finite or infinite sequence of configurations connected by δ,t -→ transitions, starting from the initial state q 0 and the initial valuation ν 0 = 0:

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • •
A run σ satisfies the Büchi condition if it visits accepting configurations infinitely often, that is configurations with a state from Acc. A duration of the run is the accumulated delay: i≥0 δ i . A run σ is Zeno if its duration is bounded.

Definition 1. The Büchi non-emptiness problem is to decide if A has a non-Zeno run satisfying the Büchi condition.

The class of TBA we consider is usually known as diagonal-free TBA since clock comparisons like xy ≤ 1 are disallowed. Since we are interested in the Büchi non-emptiness problem, we can consider automata without an input alphabet and without invariants since they can be simulated by guards.

The Büchi non-emptiness problem is known to be Pspace-complete [1].

The Zone Graph

A zone is a set of valuations defined by a conjunction of two kinds of constraints: comparison of the difference between two clocks with a constant, or comparison of the value of a single clock with a constant. For instance (xy ≥ 1) ∧ (y < 2) is a zone. The transition relation on valuations can be transposed to zones. Let -→ Z be a zone denoting the result of time elapse from Z, that is, the set of all valuations ν ′ such that ν ′ = ν + δ for some ν ∈ Z and δ ∈ R ≥0 . We have (q, Z)

t - → (q ′ , Z ′ ) if Z ′ is the set of valuations ν ′ such that (q, ν) t - → (q ′ , ν ′ ) for some ν ∈ - → Z .
It can be checked that Z ′ is a zone. Difference Bound Matrices (DBMs) can be used for the representation of zones [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF]. Transitions are computed efficiently for zones represented by DBMs.

However, the number of reachable symbolic configurations (q, Z) may not be finite [START_REF] Daws | Model checking of real-time reachability properties using abstractions[END_REF]. Hence tools like Kronos or Uppaal use an approximation operator Approx that reduces the set of zones to a finite set. The zone graph of A, denoted ZG(A), has nodes of the form (q, Approx (Z)). Observe that ZG(A) only has finitely many nodes. The initial node is (q 0 , Z 0 ) where q 0 is the initial state of A and Z 0 is the zone where all the clocks are equal to zero. The transitions of the zone graph are (q, Z)

t - → (q ′ , Approx (Z ′ )) instead of (q, Z) t - → (q ′ , Z ′ ).
It remains to define Approx in such a way that verification results for ZG(A) entail similar results for A. Let M be the maximal constant in A. M defines the precision of the approximation. We define the region equivalence over valuations as ν ∼ M ν ′ iff for every x, y ∈ X:

1. ν(x) > M iff ν ′ (x) > M ; 2. if ν(x) ≤ M , then ⌊ν(x)⌋ = ⌊ν ′ (x)⌋; 3. if ν(x) ≤ M , then {ν(x)} = 0 iff {ν ′ (x)} = 0; 4. for every integer c ∈ (-M, M ): ν(x) -ν(y) ≤ c iff ν ′ (x) -ν ′ (y) ≤ c.
The first three conditions ensure that ν and ν ′ satisfy the same guards. The last one enforces that for every δ ∈ R ≥0 there is δ ′ ∈ R ≥0 , such that valuations ν + δ and ν ′ + δ ′ satisfy the same guards. This definition of region equivalence is introduced in [START_REF] Bouyer | Forward analysis of updatable timed automata[END_REF]. Notice that it is finer than the equivalence defined in [1] thanks to the last condition which is needed for correctness of Theorem 1 below.

An equivalence class of ∼ M is called a region. For a zone Z, we define Approx (Z) as the smallest union of regions that is convex and contains Z. Notice that there are finitely many regions, hence finitely many approximated zones.

We call a path in the zone graph a finite or infinite sequence of transitions:

(q 0 , Z 0 ) t0 -→ (q 1 , Z 1 ) t1 -→ • • •
A path is initialized when it starts from the initial node (q 0 , Z 0 ). A run of A

(q 0 , ν 0 ) δ0,t0 ---→ (q 1 , ν 1 ) δ1,t1 ---→ • • • is an instance of a path if ν i ∈ Z i for every i ≥ 0.
The path is called an abstraction of the run.

Approx preserves many verification properties, and among them Büchi accepting paths as stated in the following theorem.

Theorem 1 ([15]). Every path in ZG(A) is an abstraction of a run of A, and conversely, every run of A is an instance of a path in ZG(A).

As a consequence, every run of A that satisfies the accepting conditions yields a path in ZG(A) that also satisfies the accepting conditions, and conversely. However, it is not possible to determine from a path in ZG(A) if it can be instantiated to a non-Zeno run of A. Hence, we need to preserve more information either in the automaton or in the zone graph.

Solutions to the Zenoness Problem

Theorem 1 is a first step towards an algorithm for the Büchi emptiness problem working from the zone graph. It remains to ensure that a given path in ZG(A) has a non-Zeno instance in A. Observe that the zone graph is not pre-stable: a transition (q, Z) t -→ (q ′ , Z ′ ) may not have an instance for a valuation ν ∈ Z. Hence zones are not precise enough to detect time progress.

For example, the state 3 of A 1 in Figure 1 is reachable with zone Z = (0 ≤ x ∧ x ≤ y) on path from 0 via 2. At first sight, it seems that time can elapse in configuration (3, Z). This is not the case as the transition from 3 to 0 forces x to be equal to 0. Hence, Z has to be separated in two zones: x = 0 ∧ x ≤ y that can take the transition from 3 to 0, and x > 0 ∧ x ≤ y that is a deadlock node.

We present two approaches from the literature to overcome this problem. Both are used in our algorithm in section 4. They rely on the properties of the transitions (q, Z) g;R --→ (q ′ , Z ′ ) in ZG(A). We say that a transition bounds x from above if there exists c ≥ 1 such that

- → Z ∧ g ⇒ (x ≤ c).
Observe that this is equivalent to ν ′′ (x) ≤ c for every valuation ν ′′ such that both (q, ν) δ ⇁ (q, ν ′′ ) and ν ′′ |= g. Similarly a transition bounds x from below when

- → Z ∧ g ⇒ (x ≥ c); it zero checks x when - → Z ∧ g ⇒ (x = 0)
. Finally, a transition resets x when x belongs to R. Notice that all these properties are easily checked using DBMs for zones and guards.

Adding One Extra Clock

A common solution to deal with Zeno runs is to transform a TBA into a strongly non-Zeno automaton, i.e. such that all runs satisfying the Büchi condition are guaranteed to be non-Zeno.

The construction in [START_REF] Tripakis | Checking timed büchi automata emptiness efficiently[END_REF]2] adds one clock t and duplicates the accepting states in order to ensure that at least one unit of time has passed between two visits to an accepting state. Figure 1 presents A 1 along with its strongly non-Zeno counterpart SN Z(A 1 ). The correctness of the approach comes from Lemma 1 below, the proof of which is omitted.

Lemma 1. If a path in ZG(A) visits infinitely often both a transition that bounds some clock x from below and a transition that resets the same clock x, then all its instances are non-Zeno.

The converse also holds: if A has a non-Zeno accepting run, then 1 time unit elapses infinitely often. Hence, the guard t ≥ 1 is satisfied infinitely often and there exists an accepting run of SN Z(A). By Theorem 1 one can find an accepting path in ZG(SN Z(A)).

Despite being simple, this construction may lead to an exponential blowup. It is shown in [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF] that there exists some TBA A such that the zone graph of SN Z(A) has size |ZG(A)|.2 O(|X|) . Our algorithm described in section 4 will use a similar idea as an optimization. However, no new clocks are added and no blowup is inflicted.

The Guessing Zone Graph

Another solution was introduced in [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF] in order to avoid the exponential blowup. Consider a path in ZG(A) that only has Zeno instances. Two situations may occur. Either the path has infinitely many transitions that bound some clock x from above, but only finitely many transitions that reset x. Then, the total time elapsed is bounded. Or, time cannot elapse at all because of zero-checks, as this is the case in state 3 of A 1 in Figure 1.

Zero-checks are handled thanks to a modification of the zone graph. The nodes will now be triples (q, Z, Y ) where Y ⊆ X is the set of clocks that can potentially be checked to 0. It means in particular that other clock variables, i.e. those from X -Y are assumed to be bigger than 0. We write (X -Y ) > 0 for the constraint saying that all the variables in X -Y are not 0. Definition 2. Let A be a TBA over a set of clocks X. The guessing zone graph GZG(A) has nodes of the form (q, Z, Y ) where (q, Z) is a node in ZG(A) and Y ⊆ X. The initial node is (q 0 , Z 0 , X), with (q 0 , Z 0 ) the initial node of ZG(A). There is a transition (q, Z, Y )

t - → (q ′ , Z ′ , Y ∪R) in GZG(A) if there is a transition (q, Z) t - → (q ′ , Z ′ ) in ZG(A) with t = (q, g, R, q ′ )
, and there are valuations ν ∈ Z, ν ′ ∈ Z ′ , and δ such that ν + δ (X -Y ) > 0 and (q, ν) δ,t -→ (q, ν ′ ). We also introduce a new auxiliary letter τ , and put transitions (q, Z, Y )

τ -→ (q, Z, Y ′ ) for Y ′ = ∅ or Y ′ = Y .
Observe that the definition of transitions reflects the intuition about Y we have described above. Indeed, the additional requirement on the transition (q, Z, Y )

t - → (q ′ , Z ′ , Y ∪ R)
is that it should be realizable when the clocks outside Y are strictly positive; so there should be a valuation satisfying (X -Y ) > 0 that realizes this transition. This construction entails that from a node (q, Z, ∅) every reachable zero-check is preceded by the reset of the variable that is checked, and hence nothing prevents a time elapse in this node. We call such a node clear. We call a node (q, Z, Y ) accepting if it contains an accepting state q. Figure 4 depicts the part of GZG(A 1 ) reachable from node (3, x == 0, {x, y}) with state 1 and all its transitions removed from A 1 .

Notice that directly from Definition 2 it follows that a path in GZG(A) determines a path in ZG(A) obtained by removing τ transitions and the third component from nodes.

We say that a path is blocked if there is a variable that is bounded from above by infinitely many transitions but reset by only finitely many transitions on the path. Otherwise the path is called unblocked. We have the following result.

Theorem 2 ([12]).

A TBA A has a non-Zeno run satisfying the Büchi condition iff there exists an unblocked path in GZG(A) visiting both an accepting node and a clear node infinitely often.

It is shown in the same paper that the proposed solution does not produce an exponential blowup. This is due to the fact that the zones reachable in ZG(A) order the clocks. More precisely, if Z is the zone of a reachable node in ZG(A) then for every two clocks x, y, Z implies that at least one of x ≤ y, or y ≤ x holds [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF]. Now, it can be checked that for every node (q, Z, Y ) reachable in GZG(A), the set Y respects the order given by Z, that is whenever y ∈ Y and Z implies x ≤ y then x ∈ Y . In the end, a nice polynomial bound is obtained on the size of the guessing zone graph. 4 Solving the emptiness problem on-the-fly

On-the-fly emptiness check on the guessing zone graph

We propose an on-the-fly algorithm for the Büchi emptiness problem based on Theorem 2. It requires to find an unblocked path in GZG(A) that visits both an accepting node and a clear node infinitely often. To make the presentation of the algorithm simpler, we assume that there is one distinguished Büchi condition that labels exactly all the clear nodes. Hence we search for an unblocked path in GZG(A) that satisfies the Büchi conditions.

Observe that we do not need to exhibit the path; proving its existence is simpler and sufficient1 . Our problem can thus be stated over the SCCs of GZG(A). A clock is blocking in an SCC if it is not reset by any transition in the SCC, but it is bounded from above by one of them. An SCC is unblocked when it has no blocking clock. Hence, finding an SCC that is unblocked and that contains an accepting node (for every Büchi condition) yields the required path. Conversely, from such a path, we have a satisfactory SCC.

The algorithm essentially involves three tasks: (1) detecting an accepting SCC, (2) inferring any blocking clocks in the SCC, and (3) re-exploring the SCC with blocking transitions removed. Since the blocking transitions might involve resets of other clocks, the SCCs obtained after removing blocking transitions might in turn contain new blocking clocks. These tasks have to be accomplished on-the-fly. The Couvreur's algorithm [START_REF] Couvreur | On-the-fly emptiness checks for generalized büchi automata[END_REF] finds accepting SCCs in (untimed) Büchi automata on-the-fly. We first adapt it to infer blocking clocks. Next we propose a modification to enable performing the third task. This last contribution is particularly involving. Our algorithm is depicted in Figure 2.

Couvreur's algorithm The Couvreur's algorithm, can be viewed as three functions check df s, merge scc and close scc. The algorithm annotates every node with an integer df snum and a boolean opened. The variable df snum is assigned based on the order of appearance of the nodes during the depth-first search. The opened bit is set to true when the node is just opened for exploration by check df s and is set to false by close scc when the entire SCC of the node has been completely explored. The algorithm uses two stacks Roots and Active. The Roots stack stores the root of each SCC in the current search path. The root is the node of the SCC that was first visited by the DFS. If the roots stack is s 0 s 1 . . . s n , then for 0 ≤ i ≤ n -1, s i is the root of the SCC containing all the nodes with df snum between s i .df snum and s i+1 .df snum that have opened set to true and s n is the root of the SCC containing all nodes with df snum greater than s n .df snum which have opened set to true.

The main function check df s proceeds by exploring the graph in depth-first search (DFS) order. When a successor t of the current node s is found, t.df snum being zero implies t has not been visited yet and t.opened being true implies that t belongs to the same SCC as s. When t belongs to the SCC of s, all the nodes visited in the path from t to s also belong to the SCC of s. These nodes are collected by the function merge scc, which finds the root s i of t and repeatedly pops the Roots stack so that s i comes to the top, signifying that it is the root of the SCC containing all the nodes visited from t to s. A maximal SCC is detected when all the transitions of the current node s have been explored, with s being on the top of the Roots stack. The close scc function is now called that sets the opened bit of all nodes in the SCC rooted at s to f alse. To identify these nodes, the Active stack is used, which stores all the nodes of the partially explored SCCs, in the order of the df snum.

Detecting blocking clocks Observe that each node s in the Roots stack represents an SCC rooted at s. The idea is to augment the Roots stack so that along with each node s, the set of clocks (ub) that are bounded above and the set of clocks r that are reset in a transition of the SCC rooted at s, are also stored. The set ubr gives the set of blocking clocks of the SCC rooted at s. To achieve this, SCCs are stored in the Roots stack as tuples (s, a, ub, r, ub in , r in ) where the extra sets ub in and r in store respectively the clocks that are bounded above and reset in the transition leading to s. The second modification occurs in merge scc which now accumulates these sets while popping the nodes from the Roots stack. Figure 3 gives a schematic diagram of the merging procedure.

Re-exploring blocked SCCs When a maximal SCC Γ is detected, the set ub-r of the root gives the set of blocking clocks. If ub-r is not empty, Γ needs to be re-explored with the transitions bounding clocks of blk∪(ub-r) removed. Here blk denotes the blocked clocks when Γ was being explored. Doing this would split Γ into some p smaller maximal SCCs Γ 1 , . . . , Γ p such that Γ = i=p i=1 Γ i . Each Γ i is reachable from the root of Γ . Thus, GZG(A) would have an accepting run if some Γ i contains an unblocked accepting cycle. The objective is to identify and explore the sub SCCs Γ 1 , . . . , Γ p on-the-fly. The function close scc is modified to enable on-the-fly re-exploration with blocked clocks.

Firstly, an additional bit per node called explore is needed to identify the nodes that have to be explored again. When Γ is detected and close scc called, the explore bit is set to true for all the nodes of Γ , if Γ contains blocking clocks.

The exploration is started from the root of Γ with the augmented set blk of the blocking clocks. Assume that Γ i is currently being explored with the set blk. Each time a transition s g;r --→ t is detected, check df s checks if it bounds a blocking clock, that is, a clock in blk. This way the discarded transitions are detected on-the-fly. Since t may belong to some Γ j = Γ i , it is added to the T odo stack for later re-exploration. The T odo stack is the crucial element of the algorithm. The recursion ensures that Γ i is completely closed before considering a Γ j on the T odo stack. After Γ i completes, the node t ′ on the top of the T odo stack is considered for exploration. However, it is possible that although t ′ was added due to a discarded transition, it could now belong to another SCC that has been completely closed, through a different enabled transition. Hence t ′ is explored only if its explore bit is true.

Note that it is possible that more blocking clocks are detected on some Γ i . The re-exploration on Γ i then updates the T odo stack on-the-fly. However, while popping a node from T odo, in order to identify the right set of blocking clocks it has to be explored with, a marker $ is pushed to the T odo stack whenever a new re-exploration with a new set of blocking clocks is started.

SCC 0 ub 0 , r 0 SCC 1 ub 1 , r 1 SCC 2 ub 2 , r 2 merged SCC: UB, R, ub 0 in , r 0 in ub 0 in , r 0 in ub 1 in , r 1 in ub 2 in , r 2 in ub, r U B = {ub 0 , ub 1 in , ub 1 , ub 2 in , ub 2 , ub} R = {r 0 , r 1 in , r 1 , r 2 in , r 2 , r}

On-the-fly emptiness check on the zone graph

As stated in section 3.2, the guessing zone graph construction detects nodes where time elapse is not prohibited by future zero checks. However, in the absence of zero checks, this construction is not necessary. Recall that GZG(A) has |X|+1 times more nodes than ZG(A). Therefore, it is sufficient consider the guessing zone graph construction only on maximal SCCs with zero checks. We propose an on-the-fly algorithm that checks for an accepting and unblocked SCC on the zone graph ZG(A), detects zero checks and adopts the emptiness check algorithm on the guessing zone graph only when required. The algorithm shown in Figure 2 is run on ZG(A) instead of GZG(A). When a maximal SCC Γ is detected in line 19, it is required to know if Γ contains any zero checks.

Detecting zero checks This is similar to the detection of blocking clocks. Two extra bits zc and zc in are stored along with every tuple (s, . . . ) in the Roots stack. zc in tracks zero checks in the transition leading to s and zc remembers if there is a zero check in the SCC rooted at s. When an SCC is detected, the information is merged in merge scc in a way similar to the schematic diagram shown in Figure 3. Thus when Γ is detected, the zc bit of the root reveals the presence of zero checks in Γ . The following lemma says that the algorithm can be terminated if Γ is accepting, unblocked and free from zero-checks.

Lemma 3. If a reachable SCC in ZG(A) is accepting, unblocked and free from zero-checks, then A has a non-Zeno accepting run.

The interesting case occurs when Γ does have zero checks. In this case, we apply the guessing zone graph construction only to the nodes of Γ . If (q Γ , Z Γ ) is the root of Γ , the guessing zone graph is constructed on-the-fly starting from (q Γ , Z Γ , X). Intuitively, we assume that the set of clocks X could potentially be zero at this node and start the exploration. We say that a run ρ of A ends in a maximal SCC Γ of ZG(A) if a suffix of ρ is an instance of a path in Γ . Let GZG(A) |Γ be the part of GZG(A) restricted to nodes and transitions that occur in Γ . Lemma 4. Let Γ be a reachable maximal SCC in ZG(A), with root (q Γ , Z Γ ).

A has an accepting non-Zeno run ending in Γ iff GZG(A) |Γ has an unblocked accepting SCC reachable from (q Γ , Z Γ , X).

Handling the zero checks

The function close scc is modified to identify any zero-checks in the current maximal SCC Γ that was detected. If Γ contains zero checks, then check df s is called with the node (q Γ , Z Γ , X) and the current set blk of blocking clocks. Note that the explore bit is true for all the nodes in Γ . Each time a new node t = (q, Z, Y ) of GZG(A) is discovered in the for loop s g;r --→ t, it is explored only when (q, Z).explore is true. When the exploration of GZG(A) terminates, the explore bit of all the nodes of Γ are set to f alse. The explore bit is thus responsible for the restriction of the search on GZG(A) only to the nodes that occur in Γ . In particular, this happens on-the-fly.

An optimization

We propose an optimization to the algorithm to enable quicker termination in some cases. We take advantage of clocks in an SCC that are bounded from below, that is of the form x > c or x ≥ c with c ≥ 1. We make use of Lemma 1 which says that if an SCC Γ contains a transition that bounds a clock from below and a transition that resets the same clock, then any path of Γ including both these transitions should have non-Zeno instantiations. This is irrespective of whether Γ contains zero checks. Notice that no new clock is added.

To implement the above optimization, we add clock sets lb and lb in to the Roots stack entries. The set lb keeps track of the clocks that are bounded below in the SCC. lb and lb in are handled as explained in Figure 3 for the sets ub and ub in . We also modify the condition for L(A) to be empty. We conclude as soon as an SCC, not necessarily maximal, is accepting and it bounds below and resets the same clock. Observe that it is not useful to keep track of the clocks that are bounded from below while solving zero-checks on GZG(A) as any transition that sets a lower bound in GZG(A) has already been visited in ZG(A).

The Global Algorithm and Implementation Issues

A run of our algorithm is illustrated in Figure 4. Exploring ZG(A 1 ), it computes the maximal SCC rooted at node 2 that is blocked by y. Hence, it re-explores that SCC with set of blocking clocks blk = {y}. This is seen from the double edges. Notice that the edge from node 5 to node 2 is not crossed as it is discarded by blk. The algorithm now computes the SCC Γ that contains the nodes 4, 5 and 6, that is maximal w.r.t. blk. Γ is unblocked and accepting, but it has zero-checks. Hence the algorithm explores GZG(A 1 ) starting from node (3, x == 0, {x, y}). It does not explore any transition outside of Γ . It eventually finds a non-maximal SCC in GZG(A 1 ) that proves L(A 1 ) = ∅.

Finally, we discuss memory issues for the implementation of our algorithm. Information about the SCCs in ZG(A) is stored in the Roots stack as tuples (s, a, lb, ub, r, zc, lb in , ub in , r in , zc in ). An amount of 6.|X| + 2 bits of memory is required to store the membership of each clock to the 6 sets, and the zero-check information. In the worst case, all the nodes in ZG(A) have an entry in the Roots stack. Similarly, SCCs in GZG(A) are stored as tuples (s, a, ub, r, ub in , r in ) in

ZG(A1)

Part of GZG(A1) Fig. 4. Zone Graphs of A1.

the Roots stack. 4.|X| bits allow to represent the content of those 4 sets. We estimate than the overhead due to our algorithm is 4.|X|.(|X| + 1) due to the size of GZG(A) w.r.t. the size of ZG(A).

We eventually compare to the strongly non-Zeno construction. Running the Couvreur's algorithm requires to store smaller tuples (s, a). However, the zone in s is represented by a DBM which is an |X| + 1-square matrix containing 32 bits integers. Hence, adding one clock increases the memory footprint by (2.|X| + 3).32 bits. Recall furthermore than ZG(SN Z(A)) can be 2 O(|X|) bigger than ZG(A). In the worst case all these nodes are on the Roots stack.

Experiments and Conclusion

We have implemented our algorithms in a prototype verification tool. The table below presents the results that we obtained on several classical examples. The models are products of Timed Büchi Automata that encode both the processes in the system and the property to verify. The "Zone Graph" column gives the number of nodes in the zone graph. Next, for the "Strongly non-Zeno" construction, we give the size of the resulting zone graph followed by the number of nodes that are visited during verification; similarly for the "Guessing Zone Graph" where the last column corresponds to our fully optimized algorithm.

We have considered three types of properties: reachability properties (mutual exclusion, collision detection for CSMA/CD), liveness properties (access to the resource infinitely often), and bounded response properties (which are reachability properties with real-time requirements). When checking reachability properties we would like counter examples to be feasible by real systems. This is not the case with Zeno counter examples. Hence Timed Büchi Automata offer a nice framework as they discard Zeno runs.

The strongly non-Zeno construction outperforms the guessing zone graph construction for reachability properties. This is particularly the case for mutual exclusion on the Fischer's protocol and collision detection for the CSMA/CD protocol. For liveness properties, the results are mitigated. On the one hand, the strongly non-Zeno property is once again more efficient for the CSMA/CD protocol. On the other hand the differences are tight in the case of Fischer protocol. The guessing zone graph construction distinguishes itself for bounded response properties. Indeed, the Train-Gate model is an example of exponential blowup for the strongly non-Zeno construction.

We notice that on-the-fly algorithms perform well. Even when the graphs are big, particularly in case when automata are not empty, the algorithms are able to conclude after having explored only a small part of the graph. Our optimized algorithm outperforms the two others on most examples. Particularly, for the CSMA/CD protocol with 5 stations our algorithm needs to visit only 4841 nodes while the two other methods visited 8437 and 21038 nodes. This confirms our initial hypothesis: most of the time, the zone graph contains enough information to ensure time progress.

Our last optimization also proves useful for the FDDI protocol example. One of its processes has zero checks, but since some other clock is bounded from below and reset, it was not necessary to explore the guessing zone graph to conclude non-emptiness. Conclusion and Future Work. In this paper, we have presented an algorithm for the emptiness problem of Timed Büchi Automata. We claim that our algorithm is on-the-fly as (1) it computes the zone graph during the emptiness check;

(2) it does not store the graph, in particular when it splits blocked SCCs; and (3) it stops as soon as an SCC that contains a non-Zeno accepting run is found. Our algorithm is inspired from the Couvreur's algorithm. However, the handling of bounded clocks and the application of the guessing zone graph construction on-the-fly, are two substantial increments. The previous examples are academic case studies; still they show that Büchi properties can be checked as efficiently as reachability properties for Timed Automata, despite the non-Zenoness requirement.

As a future work we plan to extend our algorithm to commonly used syntactic extensions of Timed Automata. For instance Uppaal and Kronos allow to reset clocks to arbitrary values, which is convenient for modeling real life systems. This would require to extend the guessing zone graph construction, and consequently our algorithm. Another interesting question is to precisely characterize the situations where an exponential blowup occurs in the strongly non-Zeno construction. To conclude, it can be seen that the ideas of the prototype could be used to construct a full-fledged tool like Profounder, which implements the strongly non-Zeno construction.

A Proofs

A.1 Proof of Theorem 3

Proof. The basic Couvreur's algorithm has been proved in [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF]. The T odo stack and the explore bit are the additions made to enable recursive splitting of SCCs. We first list below the invariants related to these new elements and prove them. In particular, we provide the proof that the calls to check df s made at line 16 and line 47 are correct.

Subsequently, we list all the invariants, and omit the proof details, which can be obtained based on the proof given in [START_REF] Schwoon | A note on on-the-fly verification algorithms[END_REF].

Let the latest call to check df s involved a node s and a set blk of clocks.

1. Transitions containing clocks in blk are blocking transitions.

2. For a node t, t.explore = true implies that t was found in a maximal SCC Γ that was explored with transitions upper-bounding clocks in blk Γ removed and Γ contained a set newblk Γ of blocking clocks. So t has to be explored with transitions in blk Γ ∪ newblk Γ removed. 3. The T odo stack can be considered as a sequence of nodes interleaved with the $ symbol: $ 0 s 0 0 . . . s 0 i0 $ 1 . . . $ n s n 0 . . . s n in . We number the $ symbols for clarity. Let t i be the node such that $ i was pushed during execution of line 43 of check df s(t i , -, -, blk i ). (a) t i is the root of a maximal SCC Γ i that does not contain any transition upper-bounding a clock in blk i . (b) Every Γ i has a set newblk i of blocking clocks. For 0 ≤ i < n, blk i+1 = blk i ∪ newblk i and blk = blk n ∪ newblk n . (c) For k ∈ {0, . . . , n} and j ∈ {0, . . . , i k }, s k j .explore = true implies that its explore bit was set to true during the execution of line 40 of check df s(t i , -, -, blk i ). (d) If there is a node t last last popped from the T odo stack whose check df s has not terminated, then there is a path from t last to s not containing transitions upper-bounding clocks blk. (e) When check df s(s, . . . ) terminates, all the $ symbols added during its visit are removed.

We first prove the invariants at line 12. Assume that the invariants are true before an iteration of the loop. The current node is s and the successor obtained is t. There are three cases.

-If the condition in line 13 is satisfied, t is pushed on to the T odo stack if it is not present already. Note that invariant 1 suggests that the transition from s to t contains a blocking clock. As the T odo stack is modified, we need to verify invariant 3. It is sufficient to verify only when t.explore = true.

The only change could occur in invariant 3(c). We now show that t belongs to Γ n , thus proving 3(c) after the addition of t to T odo. Since invariant 3 is true before pushing t to T odo stack, from invariant 3(c), t last belongs to Γ n . From invariant 3(d), there is a path from t last to s, not containing transitions upper-bounding clocks in blk. Hence this path does not contain transitions upper-bounding clocks in blk n too. Therefore, the path from t last to s would have been explored during the exploration of Γ n . Since t / ∈ T odo, t would have been check df s(t, . . . ) would have been called during the exploration of Γ n . Now if t.explore = true, it clearly should belong to Γ n .

-If the condition in line 15 is satisfied, we need to prove that the call at line 16 is correct. From an argument similar to above, we can infer that t belongs to Γ n . Invariant 2 and invariant 3(b), the call at line 16 is correct. -If the condition in line 17 is true, an SCC is detected and merge scc is called.

There is no change in the T odo stack and hence the invariants involving the T odo stack do not change.

We now prove the invariants at line 43. At 43, a maximal SCC with s has root has been detected. This would be the Γ n of invariant 3, with newblk n = ubr. The $ pushed now would be $ n of invariant 3. The invariants are clearly true after the addition of a $ and a node. At line 45 a node s ′ is removed from the T odo stack. From invariant 3, if s ′ .explore is true, invariant 2 proves the correctness of the call made at 47. We assume that after the call the invariants are true. From invariant 3(e), the same $ n is still the last $ symbol. Therefore, the invariants are true after the loop at line 44. The pop function performed at line 48 proves the invariant 3(e) after execution of line 48. Clearly, the rest of the invariants remain unchanged at line 48.

We now list the other invariants below and omit their proofs.

1. For a node s, s.opened = true iff s has been visited and its SCC has not been completely closed yet. 2. The Roots stack is ordered by df snum. The Roots stack is a sequence of nodes z 0 . . . z p w 0 . . . w p ′ . The sequence z 0 . . . z p represents the exploration with no blocking clocks. The sequence w 0 . . . w p ′ is the result of detecting a maximal SCC Γ which is blocked. The sequence w 0 . . . w p ′ represents the re-exploration of a sub-SCC of Γ with the set blk curr of blocking clocks. Let z Γ be the root of Γ . Then z Γ .df snum > z p .df snum.

(a) For 0 ≤ i < p, the SCC of z i contains all nodes with df snum between z i .df snum and z i+1 .df snum that have their opened set to true. (b) The SCC of z p contains the nodes with df snum between z Γ .df snum that have their opened set to true. (c) For 0 ≤ i < p ′ , the SCC of w i , with transitions blocking clocks in blk removed, contains all nodes with df snum between w i .df snum and w i+1 .df snum that have their opened set to true. The SCC of w p ′ with blocking transitions due to clocks in blk removed contains the nodes with df snum greater than w p ′ .df snum that have their opened set to true. (d) Every z i contains a set ub of clocks that are upper-bounded and a set r of clocks that are reset in its SCC found so far. Every w i again contains these two sets. 3. The Active stack contains the set of nodes whose opened bit is true. It is ordered by the order of appearance of the states during exploration.

4. Line 32 of the algorithm is executed iff an accepting unblocked SCC is found.

Complexity: A call check df s(s, . . . ) is made only when s.explore is true. For a node s, the explore bit is initially assumed to be true. Thus check df s(s, . . . ) is first called when s is first visited. It sets s.explore to f alse in line 9. Future assignments of explore to true occur in line 40 when a maximal SCC being closed has more blocking clocks. Let this set of blocking clocks be blk and this maximal SCC be Γ . If Γ is completely closed without setting s.explore to true, then s.explore can never be set to true again. Hence, if s.explore becomes true again, it can be inferred that Γ is still being explored and s.explore is set while closing a maximal SCC Γ ′ ⊂ Γ with a set blk ′ = ∅ of more blocking clocks. Therefore the next call to check df s(s, . . . ) occurs Γ ′ is explored with the set blk ∪ blk ′ of blocking clocks. Each time check df s(s, . . . ) is called with a strictly increasing set of blocking clocks. Thus the number of calls to check df s(s, . . . Proof. Consider a path in ZG(A) and one instance of the path:

(q 0 , Z 0 ) • • • {t} --→ (q i1 , Z i1 ) • • • (q i ′ 1 , Z i ′ 1 ) t≥1 --→ • • • {t} --→ (q i k , Z i k ) • • • (q i ′ k , Z i ′ k ) t≥1 --→ • • • (q 0 , 0) • • • {t} --→ (q i1 , ν i1 ) • • • (q i ′ 1 , ν i ′ 1 ) t≥1 --→ • • • {t} --→ (q i k , ν i k ) • • • (q i ′ k , ν i ′ k ) t≥1 --→ • • •
For every j ≥ 1, we have ν ij (t) = 0 and ν i ′ j (t) ≥ 1. It comes that the time that elapses on the run between steps i j and i ′ j is at least 1. Hence, the accumulated time over all steps j diverges since there are infinitely many such j. As a consequence, the time that elapses on the run diverges.

A.3 Proof of Lemma 3

Recall Lemma 3: "If a reachable SCC in ZG(A) is unblocked, free from zero-checks and accepting, then A has a non-Zeno run."

Proof. The proof is similar to Lemma 4.13 in [1]. Consider an infinite path π in the SCC of ZG(A) that is unblocked, free from zero-checks and accepting. Assume that all its instances are Zeno. Consider one particular instance ρ. Let X 0 be the clocks that are reset infinitely often on ρ. Consider a suffix ρ ′ of ρ such that:

the total amount of time that elapse on ρ ′ is less than 1; -we can identify an infinite number of configurations (q i , ν i ) on ρ ′ such that:

• all the clocks from X 0 are reset between (q i , ν i ) and (q i+1 , ν i+1 ) for all i;

• the time that elapses between (q i , ν i ) and (q i+1 , ν i+1 ) is less than 0.5.

Then, the value of the clocks outside of X 0 satisfy all the guards of the transitions on ρ ′ . The value of all the clocks from X 0 is always less than 0.5. Now, we build a non-Zero run from ρ in the following way. In every configuration (q i , ν i ) we decide to let time elapse for 0.5 time unit. This is still a run of A since:

no clock is zero-check on ρ by definition of π; -the value of all the clocks from X 0 is still less than 1, hence they satisfy the same guards; -no clock is blocking.

We deduce that A has a non-Zeno run.

A.4 Proof of Lemma 4

We recall Lemma 4: "Let Γ be a reachable maximal SCC in ZG(A), with root (q Γ , Z Γ ). A has an accepting non-Zeno run ending in Γ iff GZG(A) |Γ has an unblocked accepting SCC reachable from (q Γ , Z Γ , X)."

Proof. Let GZG(A) |Γ be the part of GZG(A) restricted to nodes and transitions that occur in Γ . More precisely, the nodes of GZG(A) |Γ are all the nodes (q, Z, Y ) of GZG(A) such that (q, Z) is a node in Γ . The transitions of GZG(A) |Γ are all the transitions of GZG(A) that connect nodes in GZG(A) |Γ .

We prove that there is an SCC in GZG(A) |Γ that is unblocked and accepting iff it is reachable from (q Γ , Z G , X).

By definition of GZG(A) |Γ , every node reachable from (q Γ , Z Γ , X) in GZG(A) |Γ is also reachable from (q Γ , Z Γ , X) in GZG(A). From (1), we also have that (q Γ , Z G , X) is reachable in GZG(A).

(q, Z)

g;R --→ (q ′ , Z ′ ) iff (q, Z, X) g;R --→ (q ′ , Z ′ , X) (1)
Hence, if an SCC is reachable in GZG(A) from (q Γ , Z Γ , X), it is also reachable from the initial node of GZG(A). By Theorem 2 A has a non-zeno accepting run (ending in Γ ). It remains to prove that if A has an accepting non-Zeno run ending in Γ , then GZG(A) has an unblocked accepting SCC reachable in GZG(A) |Γ . Consider the suffix ρ of the non-Zeno accepting run of A such that all its transitions are in Γ . It is thus an instance of a path in Γ . By Theorem 2 there exists a unblocked path π in GZG(A) that visits both a clear node and an accepting node infinitely often, and that abstract ρ. By definition, GZG(A) |Γ contains π.

The nodes that occur infinitely often on π define an SCC Γ ′ in GZG(A) |Γ . There exists a clear node (q, Z, ∅) in Γ ′ . By definition, (q, Z, ∅) is reachable from (q, Z, X) by a τ -transition. By (1), {(q, Z, X) | (q, Z) ∈ Γ } is an SCC. Hence (q Γ , Z Γ , X) can reach (q, Z, X) and (q, Z, ∅). We have an unblocked (recall π is unblocked) SCC that contains both an accepting node and a clear node that is reachable from (q Γ , Z Γ , X).

B Algorithms

Fig. 1 .

 1 Fig. 1. A Timed Automaton and a Strongly non-Zeno Timed Automaton.

Lemma 2 (

 2 [START_REF] Herbreteau | Efficient emptiness check for timed büchi automata[END_REF]). Let |ZG(A)| be the size of the zone graph, and |X| be the number of clocks in A. The number of reachable nodes of GZG(A) is bounded by |ZG(A)|.(|X| + 1).

1 function emptiness check() 2 count := 0 ; 6 functiont do 13 ifFig. 2 .

 1206132 Fig. 2. Emptiness Check Algorithm on GZG(A).

Theorem 3 .

 3 The above algorithm is correct and runs in time O(|ZG(A)|•|X| 2 ).

Fig. 3 .

 3 Fig. 3. How ub sets and r sets are merged.

  ) for every node s is bounded by |X|. The size of GZG(A) is O(|ZG(A)|.|X|). Hence the complexity of the algorithm is O(|ZG(A)|.|X| 2 ). ⊓ ⊔ A.2 Proof of Lemma 1

Fig. 5 . 1 function emptiness check() 2 count := 0 ; 4 report L(A) = ∅ 5 6

 512045 Fig. 5. The Couvreur's Algorithm for Emptiness Check of Büchi Automata.

13 mergeFig. 7 .

 137 Fig. 7. On-The-Fly Emptiness Check Functions on the Guessing Zone Graph.

  s,a,lb,ub,r,zc,lbin,ubin,rin,zcin):=pop(Roots) 1 function check scc gzg(s,ubin,rin,blk) Roots, (s,s.labels,∅,∅,ubin,rin)) --→ t s.t. t = (t ′ , Y ) and t ′ .explore do

	10	push(Roots, (s,s.labels,∅,∅,∅,⊥,lbin,
	11			ubin,rin,zcin))
	12	push(Active, s)
	13	for all s	g;r --→ t do
	2	if (s.dfsnum = 0)
	6	push(Active, s)
	7	for all s	g;r

14 if (U B(s, g) ∩ blk = ∅) and (t ∈Todo) 15 push(Todo, t) 16 else if (t.explore) 17 check scc zg(t,LB(s, g),U B(s, g), r, 18 ZC(s, g), blk) 19 else if (t.opened) 20 merge scc zg(LB(s, g),U B(s, g),r, 21 ZC(s, g),t) 22 if top(Roots) = (s,• • •) 23 close scc zg(blk) 24 25 function merge scc zg(lb ′ in ,ub ′ in ,r ′ in ,zc ′ in ,t) U:=ub ′ in ; R:=r ′ in ; Z:=zc ′ in 29 (3 count++; s.dfsnum := count 4 s.opened := ⊤; s.explore := ⊥; 5 push(8 if (U B(s, g) ∩ blk = ∅) and (t ∈Todo) 9 push(Todo, t) 10 else if (t.explore) 11 check scc gzg(t,U B(s, g),r,blk) 12 else if (t.opened)

The path is a counter-example to the emptiness of the automaton, hence it can be an expected outcome of the algorithm. ¿s in the untimed case, a short counter-example can be generated in a separate task from the outcome of our algorithm.

A:=∅;