Julio Toss

Cícero Augusto De

Lara Pahins

Bruno Raffin

João Luiz

Dihl Comba

Cícero A L Pahins

João L D Comba

Packed-Memory Quadtree: a cache-oblivious data structure for visual exploration of streaming spatiotemporal big data

published or not. The documents may come

Introduction

Advanced visualization tools are essential for big data analysis. Most approaches focus on large static datasets, but there is a growing interest in analyzing and visualizing data streams upon generation. Twitter is a typical example. The stream of tweets is continuous, and users want to be aware of the latest trends. This need is expected to grow with the Internet of things (IoT) and massive deployment of sensors that generate large and heterogeneous data streams. Over the past years, several in-memory big-data management systems have appeared in academia and industry. In-memory databases systems avoid the overheads related to traditional I/O disk-based systems and have made possible to perform interactive data-analysis over large amounts of data. A vast literature of systems and research strategies deals with different aspects, such as the limited storage size and a multi-level memory-hierarchy of caches [START_REF] Zhang | In-Memory Big Data Management and Processing: A Survey[END_REF]. Maintaining the right data layout that favors locality of accesses is a determinant factor for the performance of in-memory processing systems.

Stream processing engines like Spark [START_REF] Zaharia | Spark: Cluster computing with working sets[END_REF] or Flink [START_REF]Apache flink[END_REF] support the concept of window, which collects the latest events without a specific data organization. It is possible to trigger the analysis upon the occurrence of a given criterion (time, volume, specific event occurrence). After a window is updated, the system shifts the processing to the next batch of events. There is a need to go one step further to keep a live window continuously updated while having a fine grain data replacement policy to control the memory footprint. The challenge is the design of dynamic data structures to absorb high rate data streams, stash away the oldest data to stay in the allowed memory budget while enabling fast queries executions to update visual representations. A possible solution is the extension of database structures like R-trees [START_REF] Guttman | R-trees: a dynamic index structure for spatial searching[END_REF] used in SpatiaLite [START_REF]SpatiaLite. Spatial and geographic objects for sqlite[END_REF] or PostGis [START_REF]PostGIS. Spatial and geographic objects for postgresql[END_REF], or to develop dedicated frameworks like Kite [START_REF] Magdy | Kite[END_REF] based on a pyramid structure [START_REF] Magdy | Mercury: A memory-constrained spatiotemporal real-time search on microblogs[END_REF][START_REF] Magdy | Venus: Scalable Real-Time Spatial Queries on Microblogs with Adaptive Load Shedding[END_REF].

In this paper, we propose a novel self-organized cacheoblivious data structure, called Packed-Memory Quadtree (PMQ), for in-memory storage and indexing of fixed length records tagged with a spatiotemporal index. We store the data in an array with a controlled density of gaps (i.e., empty slots) that benefits from the properties of the Packed Memory Arrays [START_REF] Bender | Cache-oblivious b-trees[END_REF]. The empty slots guarantee that insertions can be performed with a low amortized number of data movements (O(log 2 (N))) while enabling efficient spatiotemporal queries. During insertions, we rebalance parts of the array when required to respect density constraints, and the oldest data is stashed away when reaching the memory budget. To spatially subdivide the data, we sort the records according to their Mor-ton index [START_REF] Gargantini | An effective way to represent quadtrees[END_REF], thus ensuring spatial locality in the array while defining an implicit, recursive quadtree, which leads to efficient spatiotemporal queries. We validate PMQ for consuming a stream of tweets to answer visual and range queries. Figure 1 shows the user interface prototype built to support the data analysis process. PMQ significantly outperforms the widely adopted spatial indexing data structure R-tree, typically used by relational databases, as well as the conjunction of Geohash and B +tree, typically used by NoSQL databases [START_REF] Fox | Spatio-temporal indexing in non-relational distributed databases[END_REF]. In summary, we contribute (1) a self-organized cache-oblivious data structure for storing and indexing large streaming spatiotemporal datasets; (2) algorithms to support realtime visual and range queries over streaming data; (3) performance comparison against tried and trusted indexing data structures used by relational and non-relational databases.

Related Work

In building an efficient system to enable interactive exploration of data streams, we must deal with challenges common to areas like in-memory big-data, stream processing, geospatial processing, and information visualization.

Data Structures. Data structures need to dynamically process streams of geospatial data while enabling the fast execution of spatiotemporal queries, such as the top-k query that ranks and returns only the k most relevant data matching predefined spatiotemporal criteria. One approach is to store data continuously in a dense array following the order given by a space-filling curve, which leads to desirable data locality. Inserting an element takes on average O(n) data movements, i.e., the number of elements to move to make room for the newly inserted element. The cost of memory allocations can be reduced using an amortized scheme that doubles the size of the array every time it gets full. However, elements are often inserted in batches in an already sorted array. In that case, one approach is to use adaptive sorting algorithms to take advantage of already sorted sequences [START_REF] Estivill-Castro | A survey of adaptive sorting algorithms[END_REF][START_REF] Cook | Best sorting algorithm for nearly sorted lists[END_REF][START_REF] Mcglinn | A parallel version of cook and kim's algorithm for presorted lists[END_REF]. Timsort [START_REF] Peters | Timsort[END_REF] is an example of an adaptive sorting algorithm with efficient implementations. We show experiments that compare our data structure to Timsort. Another possibility is to rely on trees of linked arrays. The B-tree [START_REF] Bayer | Organization and maintenance of large ordered indexes[END_REF] and its variations [START_REF] Brodal | Lower bounds for external memory dictionaries[END_REF] are probably the most common data structure for databases. The UB-Tree is a B-tree for multidimensional data using space-filling curves [START_REF] Ramsak | Integrating the ub-tree into a database system kernel[END_REF]. These structures are seldom used for in-memory storage with a high insertion rate. They are competitive when data access time is large enough compared to management overheads, often the case for on-disk storage. Such data structures are cache-aware, i.e., to ensure cache efficiency they require a calibration according to the cache parameters of the target architecture.

Sparse arrays are an alternative that lies in between dense arrays and trees of linked arrays. Data is stored in an array larger than the actual number of elements to store, using the extra room to make insertions and deletions more efficient. Itai et al. [START_REF] Itai | A Sparse Table Implementation of Priority Queues[END_REF] were probably the first to propose such data structure. Bender et al. [START_REF] Bender | Cache-oblivious b-trees[END_REF][START_REF] Bender | An adaptive packedmemory array[END_REF] refined it, leading to the Packed Memory Array (PMA). The main idea is that by maintaining a controlled spread of gaps, insertions of new elements can be performed moving much fewer than O(N) elements. The insertion of an element in the PMA only requires O(log 2 (N)) amortized element moves. This cost goes down to O(log(N)) for random insertion patterns. Bender and Hu [START_REF] Bender | An adaptive packedmemory array[END_REF] also proposed a more complex PMA, called adaptive PMA, that keeps this O(log(N)) for specific insertion patterns like bulk insertions. PMA is a cache-oblivious data structure [START_REF] Frigo | Cache-oblivious algorithms[END_REF], i.e. it is cache efficient without explicitly knowing the cache pa-rameters. Such data structures are interesting today since the memory hierarchy is getting deeper and more complex with different block sizes. Cache-oblivious data structures are seamlessly efficient in this context. Bender et al. [START_REF] Bender | Cache-oblivious b-trees[END_REF][START_REF] Bender | Cacheoblivious streaming b-trees[END_REF] also proposed to store a B-tree on a PMA using a van Emde Boas layout, leading to a cache-oblivious Btree. However, it leads to a complex data structure without a known practical implementation. Still, PMA has few known applications. Mali et al. [START_REF] Mali | A New Dynamic Graph Structure for Large-Scale Transportation Networks[END_REF] used PMA for dynamics graphs. Durand et al. [START_REF] Durand | A Packed Memory Array to Keep Moving Particles Sorted[END_REF] relied on PMA to search for neighbors in particle-based numerical simulations. They indexed particles in PMA based on the Morton index computed from their 3D coordinates. They proposed an efficient scheme for batch insertion of elements, while Bender relied on single element insertions. In this paper, we propose to extend PMA for in-memory storage of streamed geospatial data.

Stream Processing and Datacubes Structures. Stream processing engines, like GeoInsight for MS SQL StreamInsight [START_REF] Kazemitabar | Geospatial stream query processing using Microsoft SQL Server StreamInsight[END_REF], are tailored for single-pass processing of the incoming data without the need to keep in memory a large window of events that require an advanced data structure. The emergence of geospatial databases led to the development of a specialized tree, called R-Tree [START_REF] Guttman | R-trees: a dynamic index structure for spatial searching[END_REF], that associates a bounding box to each tree node. Several data processing and management tools have been extended to store geospatial data relying on R-trees or variations like the SpatiaLite [START_REF]SpatiaLite. Spatial and geographic objects for sqlite[END_REF] extension for SQLite or Post-Gis [START_REF]PostGIS. Spatial and geographic objects for postgresql[END_REF] for PostgreSQL. Our experiments include comparisons with both. Though such spatial libraries brought flexibility for applications in the context of traditional spatial databases, their algorithms are not adapted to consume a continuous data stream. Magdy et al. [START_REF] Magdy | Mercury: A memory-constrained spatiotemporal real-time search on microblogs[END_REF][START_REF] Magdy | Venus: Scalable Real-Time Spatial Queries on Microblogs with Adaptive Load Shedding[END_REF] proposed an in-memory data structure to query and update real-time streams of tweets. Initially called Mercury, then Venus and eventually Kite [START_REF] Magdy | Kite[END_REF] for the latest implementation (Kite is also benchmarked in our experiments). They rely on a pyramid structure that decomposes the space into H levels. Periodically the pyramid is traversed to remove the oldest tweets to keep the memory footprint below a given budget. This idea to rely on bounding volume hierarchies is also popular in computer graphics for indexing 3D objects and accelerating collision detection [START_REF] Yoon | Cache-efficient layouts of bounding volume hierarchies[END_REF]. One difficulty in these data structures is to ensure fast insertions while keeping the tree balanced. The data structure may also become too fragmented in memory leading to an increase of cache misses. The partitioning criteria are based on heuristics. There is often no theoretical performance guarantees.

Finally, we point out that several data structures were proposed recently for the visual analysis of big data. A common theme is the idea of pre-computing aggregations in datacubes proposed by Gray et al. [START_REF] Gray | Data cube: A relational aggregation operator generalizing group-by, cross-tab, and sub-totals[END_REF]. Representative work include imMens [START_REF] Liu | immens: Real-time visual querying of big data[END_REF], Nanocubes [START_REF] Lins | Nanocubes for real-time exploration of spatiotemporal datasets[END_REF], Hashedcubes [START_REF] Pahins | Hashedcubes: Simple, Low Memory, Real-Time Visual Exploration of Big Data[END_REF] and Gaussian Cubes [START_REF] Wang | Gaussian cubes: Real-time modeling for visual exploration of large multidimensional datasets[END_REF], all designed for processing static data. Streamcube [START_REF] Feng | Streamcube: Hierarchical spatio-temporal hashtag clustering for event exploration over the twitter stream[END_REF] combines an explicit spatio-temporal quadtree with datacubes for on-pass hashtag clustering. The PMQ proposes a dynamic data structure supporting the main visual queries described in these works.

Packed-Memory Quadtree

In this section, we explain the PMQ internal organization, update methods, and query types to support stream data analysis. In our description, we used as motivation dataset a stream of tweets, each with spatial location and associated satellite data. Our PMQ builds upon a PMA data structure but departs from the original one on different aspects:

• Data are indexed and sorted according to their Morton index to enforce data locality for efficient spatial queries;

• Data insertions are performed by batches in a topdown scheme to factor rebalance operations, while the PMA inserts elements one by one using a bottomup scheme;

• The PMQ has a limited memory budget. Once we reach the maximum size and density, we stash the oldest data through a customized process;

• Support for answering geospatial visual queries to allow interactive analysis of streaming datasets.

The PMQ Data Structure

We present here the PMQ data structure that strongly relies on the Packed-Memory Array [START_REF] Itai | A Sparse Table Implementation of Priority Queues[END_REF][START_REF] Bender | An adaptive packedmemory array[END_REF]. A PMQ is an array with extra space to maintain a given density of (empty) gaps between the (valid) elements. An array of size N (counting the gaps) is divided into O(N/ log(N)) consecutive segments of size O(log(N)). For convenience, the number of segments is chosen to be a power of 2. PMQ is stored in memory and keeps, for each element, an indexing key and associated value. Segments are paired hierarchically by windows following a tree structure. A level 0 window corresponds to a single segment, while the h level window encompasses the full array. The density of a window is the ratio between the number of (valid) elements in the window and its size. As we will see, the PMQ goal is to control the window densities to ensure insertion or removal of elements can be performed at low cost. The minimum and maximum density bounds for a window at level l are respectively ρ l and τ l . We define density bounds such that:

ρ 0 < • • • < ρ h < τ h < • • • < τ 0 . (1)
Thus, the larger a window, the more constraining its density bounds. The minimum and maximum densities of windows at intermediate levels are linearly interpolated between the [ρ 0 , ρ h ] and [τ h , τ 0 ] thresholds as defined below:

τ l = τ h + (τ 0 -τ h ) (h -l) h , (2)
ρ l = ρ h -(ρ 0 -ρ h ) (h -l) h , (3)
and 2ρ h < τ h . The upper (resp. lower) density threshold decreases (resp. increases) by O(1/ log(N)). This O(1/ log(N)) interval is fundamental to guarantee that an insertion or deletion requires O(log 2 (N)) amortized data movements. A valid PMQ is the one that satisfies density values for all windows. To compute a window density in constant time without having to scan its content, we associate an auxiliary accounting array to store the number of valid elements per window. This array requires an extra O(2 N log(N) ) of memory space. Figure 2 illustrates a PMQ for 9 elements. The density thresholds are: ρ 0 = 0.08, ρ 2 = 0.3, τ 2 = 0.7, τ 0 = 0.92, and the values for ρ 1 and τ 1 are defined according to Equation 2 and Equation 3.

Data Indexing

Space-filling curves define a map of multidimensional points to one dimension, which allows to order the data in a 1D array. The PMQ relies on the Morton spacefilling curve to store the elements sorted according to their Morton index. The Morton curve enables to linearly index data with 2D coordinates through a low cost bit-level operation, while preserving well the data spatial locality. Data that are close in 2D tend to have close Morton index (also called Z-index or geohash) and thus are stored nearby in the PMQ. Elements with the same Morton index are sorted according to their timestamp (e.g., tweet timestamp).

The Morton curve actually defines a recursive Z-shaped space partitioning that follows a quadtree subdivision. The ordering generated by the Morton curve is equivalent to the ordering produced by a depth-first traversal in a quadtree [START_REF] Bern | Parallel construction of quadtrees and quality triangulations[END_REF]. The number of bits used for the Z-index defines this quadtree max depth. For the PMQ, this number of bits is static. For each new incoming element, its Zindex is computed from its (x, y) position coordinates by interleaving the bits of x and y, defined according to Equation 4 and Equation 5 (note that both equations output integer values). Truncating by 2 bits a Z-index provides the index of the parent cell in the quadtree. Figure 3 illustrates a PMQ for 9 elements in a 2D domain. Elements are sorted based on their Z-index that recursively defines an implicit quadtree subdivision (never stored).

Dynamic Updates

The PMQ is designed to store a stream of data inserted by batches. The insertion starts at the topmost window of the PMQ (the full array) by checking if a violation of the density bounds occurs after inserting a batch of incoming elements. Consider a valid PMQ filled with K ordered elements. Suppose we want to insert a batch of I new elements stored in an insertion array. The goal is to insert these new elements while keeping the PMQ valid. The insertion algorithm follows a top-down approach.

If the density of the full PMQ array goes beyond τ h counting the I new elements, we first scan the array to count the number of elements with a timestamp older than a given threshold λ . If removing these elements the PMQ meets its density bounds, we remove them, rebalance evenly the remaining elements while inserting the I new elements (sorted first). Otherwise, we perform the same operation but first doubling the PMQ array size. The constraint 2ρ h < τ h guarantees that the density of this double size PMQ is above ρ h .

We now describe the batch insertion. Consider the case where inserting elements does not cause the full array density to go over τ h . Let p be the key of the first element of the right top window. We re-order the insertion array such that elements smaller than p are on the left of the insertion array, while the others are on the right. The left elements will go in the top left window of PMQ, the others in the top right window. We test for both top windows their new densities against the corresponding thresholds, counting the elements to insert. If at least one top window does not respect the density thresholds, we rebalance the elements of the full array while including the new ones, i.e., we evenly redistribute all elements. After the rebalance we have the guarantee that all windows down to segments satisfy their density bounds since densities are less constraining as the window size decreases. Otherwise, density thresholds are respected and the algorithm proceeds recursively. In the best case, rebalances only span individual segments. We update the accounting array after each batch insertion.

Note that when performing a rebalance we keep the elements sorted based on their Morton index and insertion timestamp. Since the sorting during rebalancing is stable, the only requirement is that we order the elements in the batch array by arrival time (which is the natural order in a real-time stream). Rebalancing is automatically triggered when needed. No heuristic is needed to decide when to split or delete a node as in [START_REF] Magdy | Mercury: A memory-constrained spatiotemporal real-time search on microblogs[END_REF][START_REF] Magdy | Venus: Scalable Real-Time Spatial Queries on Microblogs with Adaptive Load Shedding[END_REF]. Memory allocations are only needed when doubling the array. We control memory consumption by setting the threshold timestamp λ based on the arrival rate of the data stream.

In practice, PMQ self-stabilizes: it doubles its size until reaching a steady state where insertions and deletions balance themselves. The accounting array is updated with each window rebalance.

Notice that none of these operation use the lower densities. But they are kept in the PMQ description and supported in our implementation for completeness. They can be useful for scenarios not evaluated here. They enable to trigger window rebalances when removing elements.

The PMQ is a cache-oblivious data structure as it does not depend on cache parameters. The worst-case amortized cost is O(log 2 (N)) per insertion. The proof is given in A.

Query Types

We present three types of queries that we support in the current implementation of PMQ: heatmap, range, and topk queries. Other types of queries can be incorporated if needed.

Heatmap Queries. The visual interface of our system uses a world heatmap continuously updated based on the content stored in the PMQ (see Figure 4). An important observation is that Z-cells do not align with the tiles of the heatmap. Also, the interface allows zooming into spe- Range Queries. A range query is a spatial query that requests all elements stored in a rectangular region (Figure 5). We define a range query by the corners of a bounding box in the map. Given a range query, we have to ac-Figure 5: Heatmap zoom and range queries are used to explore the latest stream of tweets around the New York city area. The in-memory storage of PMQ provides fast access to the actual tweets' content allowing real-time user interaction even on large range queries (R = radius of the selected area). cess the PMQ to retrieve all records within the rectangular region. We return the result to the application for any post-processing of this information. In our interface, we currently display a subset of the results (e.g., a fixed number of tweets). Unlike heatmaps, which queries the PMQ using a fixed resolution grid, the range query can define an arbitrary region. Therefore, we need to find the coarsest Z-cells that contain the bounding box of the range query. Since we do not store the quadtree explicitly, we follow the Z-ordering recursively to find the Z-cells that fully enclose the bounding box. We refine each Z-cell to locate the leaf Z-cells intersecting or included in the bounding box. We refer to the book by Samet [START_REF] Samet | Foundations of Multidimensional and Metric Data Structures[END_REF] for the range query algorithm for quadtrees. Using the Z-cell indices, we locate through binary searches in the PMQ the ranges that contain the needed elements. Top-k queries. The top-k query combines the temporal ordering with the spatial dimension to find the most relevant data according to a given spatiotemporal interval. This query is processed like the range query but filters the candidate values in a temporary priority queue of size k.

Implementation

We implemented PMQ in C++. Each element has a 64-bit key representing the spatial index plus a value for storing additional information. We rely on 50-bit length Morton code for the spatial index, defining a quadtree with a fixed depth of 25 levels of refinement. The Morton index is computed from the (x, y) coordinated obtained through the EPSG:3857 projection of the longitude (lon) and latitude (lat) associated with each element, defined as:

x = lon + 180 360 .2 z , (4)
y =     1 - ln tan lat. π 180 + 1 cos(lat. π 180 ) π     .2 z-1 , (5)
where both (x, y ∈ Z | 0 ≤ x, y < 4 z ) and Z is the maximum quadtree depth.

The choice of record content to consider depends on the application needs. If only the metadata is required, we used a 16-byte struct to store latitude (32-bit float), longitude (32-bit float) and insertion timestamp (64-bit unsigned integer).

Our implementation uses PMQ segments of a fixed size of eight elements as we found no significant performance benefit in increasing the segment size with the array size. When rebalancing a window, we always pack data at the left of each segment to favor low-level optimizations like prefetching. Besides giving the window densities, the accounting array is also used to get the position of the last valid element of each segment, to avoid scanning the empty slots.

We target streaming scenarios where the PMQ is used to store the most recent incoming data sorted in memory, keeping as much data as possible for a given memory budget. Data are removed only when the PMQ is full, keeping the PMQ density high enough to avoid reducing its size (waste of memory and time as leading to a PMQ oscillating through cyclic size halving and doubling). Thus rebalances are only triggered when the window upper density bounds are reached. In our experiment we use τ 0 = 0.92 and τ h = 0.7 that give the best performance tradeoff (see Section 6.3).

Examples of Visualization Analysis using PMQ

We present an example of the interactive exploration of tweets enabled by PMQ and its user interface. The dataset consists of geolocated tweets collected with the Twitter API between November 2011 and June 2012 over the United States. The dataset has a total of 210.6 million tweets. We simulate an incoming stream of tweets by grouping them into batches of fixed size and iteratively inserting them into a given data structure.

Drill-down exploration of a Twitter stream

We provide a visual interface that allows a drill-down exploration of a tweet stream and support different queries. PMQ supports the storage in memory of the latest tweets, thus filling the gap between stream processing engines working only on a small window of the input stream, and classical solutions on persistent storage. The heatmap enables to display the concentration of tweets posted over the last hours. PMQ can index one second of tweets and keep all the elements sorted in less than 1.5 ms on average, with a maximum at about 1s when a batch triggers a top rebalance with element removal (Table 3). It is more than capable of keeping up with the stream rate and support visual queries. The interface allows the user to zoom into the heatmap or to perform range queries. We display the tweets inside selected areas in a separate area next to the map. Figure 5 shows the combined use of heatmaps and range queries at different zoom levels over New York.

The user can interactively zoom until finding the desired information.

Allert detection of regions with high tweet rates

Systems like TwitInfo [START_REF] Marcus | [END_REF] provide an interface for visualizing real-time Twitter data. Based on the user-given keyword search, the system fetches the matching twitter stream and generates an aggregated higher-level visualization, which is kept up-to-date with the incoming tweets. Such exploratory framework enables a better understanding of on-going events. However, since the stream is filtered with a fixed input keyword, it is not suitable when monitoring unexpected events. One example of an unexpected event is the monitoring of the volume of tweets in a given region. We implemented a simple pre-processing of batches to trigger alerts in regions with high tweet activity. Once an alert is triggered, the user can further investigate it by interactively exploring the last received tweets. During exploration, one can also perform top-k queries to retrieve the top-most relevant tweets at a given point. For instance, on February 5th of 2012 at 14:22 UTC, the system indicates a high tweet activity over Indianapolis. Zooming into the alert zone and using range queries, we observe that many people are at the Lucas Oil Stadium commenting about the Super Bowl game. We set a top-k query at the stadium to follow the most relevant tweets nearby. The filtered feed displayed on the right panel of the interface shows tweets with information like the teams playing (New York Giants Vs. New England Patriots), or about the Madonna's show during half-time (Figure 6).

Performance Evaluation

We created a series of benchmarks to evaluate the performance of PMQ. When possible, we showed comparisons against competing solutions from the industry and other open-source libraries. The B-Tree compared in our experiments is the stx::btree, an efficient open source implementation of in-memory B+Tree [START_REF] Bingmann | STX B+ Tree C++ Template Classes v0[END_REF]. The R-Tree implementation is from the Boost C++ template library [START_REF]Boost. Geometry Index[END_REF]. We conducted the experiments to allow reproducing results and exploring different parameter configurations.

We created a GitHub repository to store supplemental material and additional benchmarks 1 . The benchmarks were run on a dedicated Linux machine with an Intel i7-4790 CPU @ 3.60GHz with 32GB of main memory.

Evaluating Storage Solutions for Spatial Data

We conducted a set of experiments to evaluate PMQ against two different storage solutions for spatial data. The first type of storage solution is traditional open source relational databases (RDBMS) with geospatial library extensions, such as: (1) in-memory SQLite + SpatiaLite and (2) PostgreSQL + PostGIS. SQLite uses in-memory storage, while PostgreSQL uses a disk. Typically, RDBMS store entries in a table and build an additional spatial index separately. This optional index supports efficient spatial queries that contain geometric predicates. The second storage solution are dense vectors using a pointer-based quadtree index on a dense C++ std::vector. Spatial ordering in the container uses two sorting algorithms: (1) the C++ std::sort() implementation from GNU GCC libstdc++ and (2) the C++ TimSort [START_REF] Goro | Timsort[END_REF] adaptive sorting algorithm. This set of benchmarks gives an insight into the scalability of insertion and query operations of the solutions above. The different data structures are initially empty and increase their size as elements arrive in batches. We measured the insertion time of each batch, including the time for updating the index (in case of RDBMS) and physically storing the data. We also measured the time for 1 https://github.com/pmq-authors/pmq-extras accessing data from the storage. After each batch insertion, we queried all elements indexed by the data structure (Figure 7). As can be seen, even with a small number of elements, the database solutions have poor scalability. While PostGIS uses disk storage, it spends most of the time optimizing the index and physically reordering elements on disk. SpatiaLite, on the other hand, seems to have a less efficient indexing strategy than PostGIS. It spends less time on indexing and insertion operations, but pays a significant cost to access the data, even if stored in memory. None of the database solutions are suited to the real-time latency requirements of update and read operations. The spikes on PMQ benchmarks correspond to doubling the array size when the structure reaches the maximum density. The sparse storage of PMQ allows reducing the time on insertion when compared to the dense vectors. In the next experiments, we remove the database solutions from the comparisons since they are an order of magnitude slower than the vector-based storage approaches, and compare against low-level structures such as B-trees and R-trees.

Evaluating Insertions

We evaluate the scalability of the data structures by comparing their trade-offs between insertions and scanning operations. These two operations represent a performance compromise of two conflicting workloads. While treebased data structures, like B-Tree and R-Tree, show good insertion performance (Figure 8(a)), they fail in maintaining in-memory data locality, which has a significant impact on scanning operations (Figure 8(b)). The solution using dense sorted vectors reveals the importance of data locality when scanning. We derive the lower-bounds of scanning performance when we achieve the best locality. However, its update costs for frequent insertions make it impracticable for large amounts of data. PMQ shows a good compromise between these two operations. On insertions, it performs similarly to the R-Tree, it is 2X times slower than the B-Tree and scales logarithmically with the size of the data structure. At the same time, PMQ pays only a small constant overhead relative to best possible scanning data-structure, the dense vector. Compared to the tree-based data-structures, with 10 M elements, the scan operations on PMQ are 3X times faster than B-Tree and 5X faster than R-Tree.

Evaluating Bulk Deletions

In the case of streaming data, the memory available limits the storage of information. We used a stashing procedure to evict old data while receiving new incoming records. Data structures are in a steady regime if they cannot grow after inserting a given number of records. At this point, a bulk removal is triggered to remove a number of the oldest elements in the data structure, given by the threshold parameter λ . How often removals are triggered depends on the rate of the incoming stream and the threshold λ . We keep the incoming rate constant by inserting a batch of 1000 elements at each simulation step. Because the bulk removal is slower than regular insertions, the choice of λ has an impact in two performance indicators: the average execution time of each operation (Figure 9(a)) and the bulk removal execution time (Figure 9(b)). To evaluate the indicators and choose the best λ , we insert in each structure a dataset of nearly 46 million elements and set the maximum number of elements to be stored to half of this size. Figure 9 shows running times for λ varying from 0.1% to 50% of the maximum capacity. For both the B-Tree and the R-Tree, the removal size has to be chosen carefully to balance the time spend on each removal operation and the total running time. If the removal size is large (over 3.13%), each operation deletes many elements at once causing expensive removal operations that take over 1 second (black horizontal line in Figure 9(b)). If the removal size is small (under 0.78%), each removal is fast since only a small percentage of elements are evicted. However, it increases the frequency of removals impairing the total running time (Figure 9(a)). In opposite, the PMQ triggers element removal automatically when the top density threshold is reached. As a consequence, the execution time of removals is much less sensitive to λ . As Figure 9(b) shows, for any removal size, the running time is under one second. As expected, the total running time for all structures is best with larger and less frequent In Table 1, we summarize the results from Figure 9(a) and Figure 9(b). We show, for each structure, the best tradeoff between removal and average running time. The B-Tree and R-Tree require a small removal percentage (λ ), while PMQ removes 50% of if elements and it is 2× faster for both removal and average running time. In Table 2, we take the λ value that gives the best performance tradeoff for the B-Tree and set it to the other data structures. Once again, PMQ performs best and is the only one to make removal operations in less than a second. In Figure 10 we compare several values of τ h threshold (with fixed τ 0 = 0.92) for the PMQ at steady regime: when the PMQ density reaches τ h a bulk removal is triggered keeping at least 10.8 M elements. The value τ h = 0.7 gives the best average insertion time. The PMQs with τ h = 0.5 and 0.6 require twice more storage memory compared to the ones with 0.7, 0.8 and 0.9, with a high average insertion time. High τ h values (0.8 and 0.9) leave the PMQ fill, leading to costly rebalances of large windows. The value τ h = 0.7, chosen for all our other experiments, gives the best average insertion time with low memory footprint. A high value τ 0 = 0.92 gives the best results, allowing some local high-density spots.

Evaluating the Rebalancing Procedure

PMQ supports a rebalancing procedure that is only activated when necessary. In Table 3 we simulate a tweet insertion rate of 1000 tweets per second. We present the average insertion time in PMQ after reaching a steady state (i.e. after the first top-level rebalance that started removing tweets). Notice that during this steady state, elements deletion neither leads to halving nor doubling the PMQ size. Between the top two level rebalances, the number of elements in the container varies from Elts min to Elts max. The maximum value in the table corresponds to a single insertion that triggers a top-level rebalance. Although these periodic rebalances can take up to one second, this latency is hidden from the user as the mean insertion time (and the 99th percentile) is much smaller than the insertion rate.

We also evaluated how PMQ scales with varying insertion rates. We used a time window of 6 hours and increase the insertion rate up to 8k tweets/s. Figure 11 shows the average insertion time and standard deviation. PMQ takes less than 8 ms to digest 6000 tweets per second, the current average number of tweets posted per second worldwide [START_REF] Stats | Twitter usage statistics[END_REF].

Figure 11: PMQ average insertion time with a window of 6h and varying rates. Current Twitter insertion rate (6K tweets/s) can be processed under 7.5 ms.

Evaluating Range Queries

We evaluated the range query performance of the different data structures. We defined synthetic queries at varying sizes and different positions to simulate searches over the world map. Queries are defined using latitude and longitude coordinates over a rectangular map of the world using the Mercator projection. Each query is specified by its center latitude and longitude coordinates (lat, lon), where lat ∈ ℜ -90,+90 and lon ∈ ℜ -180,+180 , and by its width W = {w ∈ ℜ : w = 90 2 i ∧ 0 ≤ i < 8}. For each w in W , we randomly pick ten tweet coordinates from the dataset to generate a unique query. We discarded queries not fully contained on the world map. As a result, the query dataset we built has 80 queries. This set of queries was run over 8 different datasets at varying sizes from 1M to 128M elements, for a total of 640 query results. The size of the dataset is given by a parameter S defined as {1M × 2 i : 0 ≤ i < 8}. We performed each query 10 times and computed the average running time. Since we fixed the number of elements in memory, we computed the throughput of each query as the number of records returned by the query divided by the running time (in ms).

We compared the throughput by showing the speedup of PMQ over B-Tree and R-Tree (Figure 12). The boxplots in Figure 12 show the speedup grouped by w. The labels on the x-axis show the range query coverage relative to the total area of the domain. PMQ and B-Tree use the same querying mechanism based on the recursive space partitioning of a quadtree. In this case, PMQ is always better than the B-Tree, with speedups that can achieve up to 7× on the largest range queries. The speedup over the B-Tree is proportional to the number of elements returned by the query and is mainly due to the memory locality of PMQ. When the number of elements scanned to answer a query increases, the B-Tree has to access nodes scattered in memory locations, thus causing a poor usage of the cache memories. The average speedup increases with the range query size. Since the R-Tree is a pointer-based data structure, its internal nodes have bounding boxes containing the space occupied by its children, and only leaf nodes have the actual elements. Because of its internal index, the R-Tree is efficient for point queries, with good performance when a small amount of elements is queried. In a streaming dataset, elements are inserted individually in the data structure, as they arrive from the stream and without any specific ordering in memory. When the size of the range queries increases, the cost of scanning more elements hinders the throughput. The query algorithm uses a max depth parameter to limit the refinements done in the linear quadtree. The max depth of 10 used in this experiments was found to give the best results (for B-Tree and PMQ) as shown in Figure 13. The refined quadrants that do not fall entirely inside the queried region are scanned linearly to test the elements contained in the queried region. As a consequence, small range queries in regions with a high density of elements suffers from discontinuities in the Z-curve ordering. The throughput has a negative impact when the number of valid elements returned is low compared to the number of records scanned. Despite this, in our experiments the PMQ query algorithm outperforms the R-Tree (which does not rely on a Z-curve) by 5.5 times in 97% of the largest range queries.

-3 2 -1 2 1 2 2 2 3 2 -3 2 0 2 3 2 -3 2 0 2 3 2 -6 2 -3 2 0 2 0 2 2 2 -6 2 -4 2 -2
-3 2 -1 2 1 2 2 2 3 2 -3 2 0 2 3 2 -3 2 0 2 3 2 -6 2 -3 2 0 2 0 2 2 2 -6 2 -4 2 -2

Evaluating Top-k Queries

We compared the performance of top-k queries implemented on top of our PMQ against the Kite framework [START_REF] Magdy | Kite[END_REF]. We generated 10K top-K queries from the check-in locations of the Brightkite social network [START_REF] Leskovec | Snap datasets: Stanford large network dataset collection[END_REF]. Queries shows queries for different latency values. PMQ answers 90% of the queries in less than 4 ms while Kite can only process 3% of it. Kite uses a regular grid as a spatial index. Since the grid does not change to adapt to the complexity of the data, Kite does not perform well under scenarios of streaming datasets. The data being sorted first based on their Z-index and next their timestamp, a pure time based query with no spatial constraint would need to scan all the elements of PMQ. We have seen that the PMQ shows a good scan performance (Fig. 8(b)). But if a majority of requests of this type are expected it may be advantageous to index data based on their timestamp first.

Evaluating Memory Usage

We measured the amount of resident set size used by each data structure individually (e.g., the physical memory used by the process code and data). The Linux Kernel maintains a pseudo-file system directory for each running process. By parsing /proc/self/statm we have access to the current resident set size in pages. We multiply this value by the page size from sysconf() to obtain the amount of used memory in bytes. We set the record size to 16 bytes, the minimum space required to store spatial and timestamp metadata. Each batch inserts 1000 records per iteration. For every iteration, we measured the current resident set size used by the data structures. Memory usage in a dense vector is directly proportional to the number of records, as shown in Figure 15, and serves as a baseline since this alternative does not have any storage overhead. PMQ memory usage depends on the max density parameter, τ h (see Section 3.1). In our experiments τ h is configured to 0.7, i.e., the used memory slots correspond at maximum to 70% of slots allocated. As the number of elements in the data structures increases, PMQ doubles its size when the maximum density is reached (note the staircase-shaped curve of PMQ in Figure 15). In the experiments of Section 6.3, the maximum number of elements presented in memory was 23.488.000, which corresponds to the memory consumption show in Table 4.

Discussion of the Evaluation Results

The design of a data structure that is at the same time efficient for insertion/removal operations and large range queries requires careful analysis of trade-offs. Experiments have shown that PMQ offers a good tradeoff between both types of workloads. At a steady regime PMQ can perform efficient bulk removals, which are usually expensive in tree-based data structure because they require a full scan of the data. The execution of queries in PMQ is substantially different from R-Trees because there are no index pointers to locate records. Instead the PMQ keeps data sorted based on Z-indices, and it suffices to use a fast range searching algorithm. We used the same Z-order in PMQ and B-Tree. However, as data is inserted and removed dynamically, a tree structure becomes fragmented in memory. PMQ avoids this issue by keeping the locality of its records along the Z-curve. Our experiments always verified that PMQ outperforms the B-Tree.

Some insertions in the PMQ can lead to higher execution times when a full rebalance is required: when the PMQ size needs to be doubled (Figure 7), or, with a lesser impact, at steady regime during bulk data removals (Fig-ure 10). To mitigate the impact on query response time, one could rely on multithreading to overlap as much as possible rebalances with queries, adapting the approach proposed in [START_REF] Bender | Cache-Oblivious B-Trees[END_REF] for the PMA.

Conclusion and Future Work

We introduced PMQ, a new data structure to keep sorted a stream of data that can fit in a controlled memory budget. PMQ reorganizes itself when needed with a low amortized number of data movements per insertion (O(log 2 (N))). Amongst the data structure compared, PMQ, B-Tree, and R-Tree, PMQ proved to have the best performance trade-off between insertion and searching times. Experiments showed that PMQ enables querying a continuously updated window with the latest arrived tweets in real-time. PMQ can maintain a significant amount of data in memory, filling the gap between stream processing engines working only on small windows of received stream, and other classical persistent storage solutions.

One direction for improvement would be to combine in-memory and persistent storage in a multi-level PMQ. The lazy stashing protocol might not adapt to some needs, as old data may stay a long time (up to the next top rebalancing) before being removed. We plan to develop a more reactive protocol for such situations. The current implementation imposes that every operation must acquire a thread lock before accessing or modifying PMQ. All requests are thus performed sequentially, which limits the number of transactions that PMQ can support.

Figure 1 :

 1 Figure 1: A Twitter stream is consumed in real-time, indexed and stored in the Packed-Memory Quadtree. (a) : live heat-map displays tweets in the current time window. (b) : alerts indicate regions with high activity of Twitter posts at the moment. (c) : the interface allows to drill-down into any region and query the current data. (d) : the actual data can be retrieved from the Packed-Memory Quadtree to analyze the tweets in the region of interest.

Figure 2 :

 2 Figure 2: PMQ with 4 segments: ρ l and τ l are the minimum and maximum densities allowed at each level l of PMQ, d the actual window density. The numbers in circles count the valid element per window and are stored in the PMQ accounting array.

Figure 3 :

 3 Figure 3: PMQ storage of 9 z-indexed elements from a 2D domain (right). Z-indices correspond to a quadtree actually never built as z-index are directly computed by interleaving their x-y bits (Right).

Figure 4 :

 4 Figure 4: The heatmap is updated dynamically as the stream of tweets is received. With an average insertion rate of 1000 tweets/sec we show the heatmap when PMQ contains 100K (left) or 10M (right) elements.

  Given a 2D point p, the top-k query finds the elements with k lowest values according to a score function. The search space of the top-k queries can be reduced using both spatial and time thresholds. The parameter R defines a radius where records are going to be ranked by distance to p. Similarly, the parameter T limits the oldest timestamp to consider in the scoring function. Both scores are then normalized and combined into a final score to balance the importance of the spatial and temporal dimensions. Elements in the same Z-cell (i.e., with the same Morton code) are ordered based on their timestamp. The top-k search uses the same refinement algorithm as for range queries to find the records included inside the bounding box of radius R centered at p. We insert the returned elements into a priority queue of max-size k ordered by the spatiotemporal score to keep only the k elements with the highest score.

Figure 6 :

 6 Figure 6: Allert detection: triggers configured by the user show alerts (yellow squares) on several cities with a high rate of tweet arrival during Super Bowl 2012. We select the Indianapolis region (where the game occurs) and filter tweets using a top-k query to retrieve the most relevant tweets in the area.

Figure 7 :

 7 Figure 7: Performance comparison of spatial data storage solutions. Top row: standard geospatial databases can not handle real-time insertions. Bottom row: in-memory containers based on dense or sparse (PMQ) vectors.

  (a) Insertion of 10M elements by batches of 1000 elements. (b) Time for a full scan of the dataset after each batch insertions.

Figure 8 :

 8 Figure 8: Scalability insertion and scan operation.

  Average time of each bulk removal operation.

Figure 9 :

 9 Figure 9: Steady data regime: deletions are performed periodically. For each test, we insert a dataset of 46 million elements. The maximum number of elements allowed is half of the dataset size (around 23 million elements), and removals are configured with different percentages of the maximum.

Figure 10 :

 10 Figure 10: PMQ performance at steady regime for different τ h thresholds.

Figure 12 :

 12 Figure12: Range queries: PMQ speedup over the B-Tree and R-Tree. Each boxplot represents the speedup of throughput for each query instance. The average speedup is denoted by red crosses. PMQ is faster than the B-Tree in all cases. Compared to the R-Tree, PMQ has a speedup on 97% of queries tested. The cases where PMQ performs worst corresponds to queries returning a small number of elements compared to the dataset size.

Figure 13 :

 13 Figure 13: Examples of Range Queries. We define 8 different query widths. The B-Tree and PMQ use 10 levels of quadtree refinement for range queries. We choose this parameter experimentally to provide the best overall results.

Figure 14 :

 14 Figure 14: Top-k Queries: cumulative percentages of query latency for K = 100 , R = 30 km and T = 10000 seconds. We compared the search performance of PMQ against the Kite framework.

  Figure

14

 14

Figure 15 :

 15 Figure 15: PMQ memory usage depends on density thresholds 2ρ h < τ h . Boost C++ R-Tree has a bigger index overhead than stx::btree.

Table 1 :

 1 Parameter λ set for the best relation of removal RM time and average Avg runnning time for each algorithm.

	Avg. Run	RM

Table 2 :

 2 Comparison using same λ optimized for the B-Tree.

	λ	Elts min	Elts max Mean	99%	Max
	3h 10.8 * 10 6	11.74 * 10 6	1.209 1.066	265.613
	6h 21.6 * 10 6	23.48 * 10 6	1.310 1.134	554.971
	9h 32.4 * 10 6	46.97 * 10 6	1.278 1.587 1007.040
	12h 43.2 * 10 6	46.97 * 10 6	1.423 1.321 1045.950

Table 3 :

 3 Insertion time of batches of 1K elements in a PMQ with different time-windows λ . The number of elements in the container varies from Elts min to Elts max. The Mean, 99% and Max times are in ms.

Table 4 :

 4 Memory usage summary

		Number of Elements stored
	Algorithm	11.7 M Elts	23.4 M Elts
	Dense Vector 275.32 MB	545.97 MB
	PMQ	882.97 MB	882.97 MB
	B-Tree	477.00 MB	951.63 MB
	R-Tree	510.42 MB	1019.15 MB

Acknowledgment

The authors wish to thank the anonymous reviewers for their valuable comments and suggestions to improve the quality of the paper. This work was supported in part by CNPq 308851/2015-3 and CNPq 140313/2017-6.

A Proof of the PMQ Amortized Cost

Let first identify an important property on windows densities after rebalance. A j-level window w j is rebalanced when overfull (d(w j ) > τ j )). The rebalance occurs at the smallest underfull upper window w l with l > j, i.e. the smaller one checking d(w l ) < τ l )). In worst case this is a top level rebalance requiring to double the PMQ size.

After rebalance the density of w j checks:

by Equation 1 of page 4. So w j gets a density d(w j ) < τ j+1 . Now let consider a window w j and let see how many insertions are necessary in this window so that it triggers a rebalance, i.e. it requires to rebalance the parent window w j+1 . We assume w j just get rebalanced, thus d(w j ) < τ j+1 by Equation 6. The next rebalance triggered by w j occurs once d(w j ) > τ j , i.e. after the insertion of (τ jτ j+1 )2 j K elements where K = O(log(N)) is the segment size.

Such rebalance requires to move 2 j+1 K elements. If the rebalance occurs at the root window ( j = h), the PMQ first makes a full scan of the PMQ to identify the data to be stashed. These data are next removed during the rebalance that is either performed on w h = O(N) if the new density is bellow τ h or on a twice larger window after doubling the PMQ size. Thus a root rebalance cost is bounded by 2 h+2 K. We also need to count the cost of updating the accounting array. Each rebalance triggered by w l leads to update 2 j+2 -1 + h -( j + 1) elements of the accounting array.

Putting all these costs together, we have a cost associated to a rebalance triggered by w j bounded by:

This leads to the amortized cost per insertion of:

by Equation 2 of page 4. When an element is inserted into the PMQ, it actually contributes to the density of all enclosing windows from the segment up to the root, i.e. of h = O(log(N)) windows. The amortized rebalance cost per insertion into the PMQ is thus O(log 2 (N)).

Each element needs to be inserted in the right place in the PMQ. If inserted one by one a binary sort is used with cost O(log(N)). If inserted by batches, the insertion array is sorted with a cost per element that is also bounded by O(log(N)). Added to the amortized rebalance cost, we get an unchanged total amortized cost per insertion of O(log 2 (N)).


Serdar Erbatur
email: serdar.erbatur@imdea.org

Andrew M Marshall
email: marshall@umw.edu

Christophe Ringeissen
email: christophe.ringeissen@loria.fr

Knowledge Problems in Equational Extensions of Subterm Convergent Theories (Extended Abstract)

We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In this note we extend this to consider a subterm convergent equational term rewrite system defined modulo an equational theory, like Commutativity or Associativity-Commutativity. We show that for certain classes of such equational theories, namely the shallow classes, the two knowledge problems remain decidable.

Introduction

Verifying the security of protocols requires the development of specific decision procedures to reason about the knowledge of an intruder. Two important measures of this knowledge are (intruder) deduction [START_REF] Millen | Constraint solving for bounded-process cryptographic protocol analysis[END_REF][START_REF] Paulson | The inductive approach to verifying cryptographic protocols[END_REF] and static equivalence [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. The deduction problem is the question of whether an intruder, given his deductive capability and a sequence of messages representing their knowledge, can obtain some secret. This is a critical measure of the capability of the protocol to maintain secrets. Deducibility is needed for many questions about the security of protocols. However, there are some questions for which we need to be able to decide more than deducibility. For some protocols, in addition to deducibility, we would like to determine whether an intruder can distinguish between different runs of the protocol. For example, in protocols which attempt to transmit encrypted votes we would like to know if, to the attacker, two different votes are indistinguishable. Static equivalence measures this property.

Much work has gone into investigating and developing decision procedures for the deduction and the static equivalence problems [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Baudet | YAPA: A generic tool for computing intruder knowledge[END_REF][START_REF] Conchinha | FAST: an efficient decision procedure for deduction and static equivalence[END_REF][START_REF] S ¸tefan Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF][START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF]. In this work the security protocols are often represented by equational theories with the theories of interest usually defined as unions of several simpler sub-theories. In this paper, we focus on decision procedures for the deduction problem and the static equivalence problem in equational theories E = E 1 ∪E 2 where E 1 and E 2 are possibly non-disjoint. Until now, the following scenarios have been successfully investigated: E 1 is given by a subterm convergent term rewrite system, and E 2 is empty [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]; E 1 and E 2 are disjoint [START_REF] Cortier | Decidability and combination results for two notions of knowledge in security protocols[END_REF]; E 1 and E 2 share only constructors [START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF]. In this paper, we consider the case where E 1 is given by a term rewrite system which is both subterm and convergent modulo E 2 . We then show that the methods of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] can be extended to subterm convergent rewrite systems for a significant class of E 2 theories.

Preliminaries

We assume the reader is familiar with equational unification and term rewrite systems. We review some critical definitions below but a more complete overview can be found in [START_REF] Baader | Term rewriting and all that[END_REF].

A finite convergent term rewrite system (TRS) R is said to be subterm convergent if for any l → r ∈ R, r is either a strict subterm of l or a ground term. An equational theory is subterm convergent if it is presented by a subterm convergent TRS.

The size of a term t is denoted by |t| and defined in the usual way as follows:

|f (t 1 , . . . , t n )| = 1+Σ n i=1 |t i | if f is a n-ary function symbol with n ≥ 1, |c| = 1 if c is a constant, and |x| = 0 if
x is a variable. The size of a TRS R is denoted by |R| and defined as follows: |R| = max {l→r∈R} |l|. Since a variable cannot occur as the left-hand side of any rule in R, we have that |R| ≥ 1 for any non-empty TRS R. When R is empty, we define |R| = 1.

Equational Theories. Let us introduce the different classes of theories considered in the paper. An equational theory E is finite if for each term t, there are only finitely many terms s such that t = E s. Matching in finite theories is finitary. A sufficient condition to get a finite theory is to assume that E is permutative. An equational theory E is permutative if for each axiom l = r in E, l and r contain the same symbols with the same number of occurrences. Well-known theories such as Associativity (A), Commutativity (C), and Associativity-Commutativity (AC) are permutative theories. Unification in permutative theories is undecidable in general [START_REF] Schmidt-Schauß | Unification in permutative equational theories is undecidable[END_REF].

A theory E is syntactic if it has a finite resolvent presentation S, that is a finite set of equational axioms S such that each equality t = E u has an equational proof t ↔ * S u with at most one step ↔ S applied at the root position. A theory E is shallow if variables can only occur at a depth at most 1 in axioms of E. Shallow theories are syntactic theories for which unification is finitary [START_REF] Hubert Comon | Syntacticness, cyclesyntacticness, and shallow theories[END_REF]. The theory AC is permutative and syntactic, while C is permutative and shallow.

Notions of Knowledge. The applied pi calculus and frames are used to model attacker knowledge [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. In this model, the set of messages or terms which the attacker knows, and which could have been obtained from observing one or more protocol sessions, are the set of terms in Ran(σ) of the frame φ = ν ñ.σ, where σ is a substitution ranging over ground terms. We also need to model cryptographic concepts such as nonces, keys, and publicly known values. We do this by using names, which are essentially free constants. Here also, we need to track the names which the attacker knows, such as public values, and the names which the attacker does not know a priori, such as freshly generated nonces. ñ consists of a finite set of restricted names, these names represent freshly generated names which remain secret from the attacker. The set of names occurring in a term t is denoted by f n(t).

Definition 1 (Deduction Problem [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]). Let φ = ν ñ.σ be a frame, and t a ground term. We say that t is deduced from φ modulo E, denoted by φ E t, if there exists a term s such that sσ = E t and f n(s) ∩ ñ = ∅. The term s is called a recipe of t in φ modulo E.

Another form of knowledge is the ability to tell if two frames are statically equivalent modulo E, sometimes also called indistiguishability.

Definition 2 (Static Equivalence [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]). Two terms s and t are equal in a frame φ = ν ñ.σ modulo an equational theory E, denoted (s = E t)φ, iff sσ = E tσ, and ñ ∩ (f n(s) ∪ f n(t)) = ∅. Two frames φ = ν ñ.σ and ψ = ν ñ.τ are statically equivalent modulo E, denoted as φ ≈ E ψ, if Dom(σ) = Dom(τ ) and for all terms s and t, we have (s = E t)φ iff (s = E t)ψ.

Both deduction and static equivalence are known to be decidable in subterm convergent theories [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. In the following, we lift this result to term rewrite systems that are subterm convergent modulo some equational theory.

3 Subterm Equational Convergent TRS

Consider (Σ, E) = (Σ 1 ∪ Σ 2 , R 1 ∪ E 2 ) where (Σ 1 ∪ Σ 2 , R 1 ) is a TRS modulo a finite theory (Σ 2 , E 2 ) (for instance Σ 2 = {+} and E 2 = AC(+)).
The rewrite relation of R 1 modulo E 2 is defined as usual: s → R1,E2 t if there exist some position p in s, some rule l → r ∈ R 1 and a substitution µ such that s| p = E2 lµ and t = s[rµ] p . We assume that → R1,E2 is convergent modulo E 2 [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF]. This implies the uniqueness of normal forms modulo E 2 and the decidability of the word problem modulo E: for any terms s and t, we have s

= E t iff (s ↓ R1,E2 ) = E2 (t ↓ R1,E2 ).
In the following, we say that a term or a substitution is normalized if it is normalized w.r.t → R1,E2 . A frame φ = ν ñ.σ is said to be normalized if σ is normalized. Definition 3. Let Σ 1 and Σ 2 be two disjoint signatures, and

(Σ 2 , E 2 ) a finite theory. A subterm E 2 -convergent TRS (Σ 1 ∪ Σ 2 , R 1 ) is a TRS such that → R1,E2 is convergent modulo E 2 and for any l → r in R 1 , l is not Σ 2 -
rooted and r is a strict subterm of l or a ground term.

Example 1. The following TRSs are subterm AC(+)-convergent:

{occ(x + k, k) → ok} {rm(x + k, k) → x} {dec(enc(x, k + y), k) → x} {dec(enc(x, k), k + y) → x}
In the case of subterm convergent TRSs (modulo the empty theory), the decision procedure for the deduction problem computes deducible terms among the set of subterms occurring in the frame. When considering a non-empty theory E 2 , we have to introduce an extended notion of subterm to capture the fact that matching modulo E 2 is now performed when applying a rewrite step modulo E 2 .

In the rest of this section we assume that E 2 is both permutative and syntactic. While this may seem somewhat restrictive it allows for the consideration of theories such as AC and C which are found in a large number of security protocols. Both AC and C are indeed syntactic theories [START_REF] Kirchner | Syntactic theories and unification[END_REF].

Given a term t, St(t) is the finite set of terms in t inductively defined as follows: The following result states that we cannot generate a new term outside St(t) by rewriting terms in St(t) (except the ground right-hand sides of R 1 ). Lemma 1. If lσ = E2 t, then for any position p of l, (l| p )σ ∈ St(t).

St(t) = {t | t = E2 t} ∪ t t ∈ St(x i σ), f (x 1 , . . . , x m )σ = E2 t, f ∈ Σ 1 ∪ Σ 2 x 1 , . . . ,

Proof. By structural induction on l.

If l is a variable, this is trivial since the only possible position is and l| = l. Assume l = f (l 1 , . . . , l m ) and σ is a substitution such that f (l 1 , . . . , l m )σ = E2 t.

If there is an equational step at the root position, then there exist some terms g 1 , . . . , g m such that l 1 σ = E2 g 1 , . . . , l m σ = E2 g m and f (g 1 , . . . , g m ) = E2 t. By definition of St(t) and Proposition 1, the terms g 1 , . . . , g m are in St(t), and so l 1 σ, . . . , l m σ ∈ St(t).

If there is no equational step at the root position, then t is of the form f (t 1 , . . . , t m ) and l 1 σ = E2 t 1 , . . . , l m σ = E2 t m . By definition of St(t) and Proposition 1, the terms t 1 , . . . , t m are in St(t), and so l 1 σ, . . . , l m σ ∈ St(t).

Decision Procedures

From now on, we assume that E 2 is a shallow permutative theory, e.g., Commutativity.

Deduction. The decision procedure for the deduction problem requires the computation of some finite deducible terms defining the so-called completion of a given frame. Definition 4. Let φ = ν ñ.σ be a normalized frame. The set of local deducible terms in φ is the smallest set D such that:

• Ran(σ) ⊆ D, • if t 1 , . . . , t n ∈ D and f (t 1 , . . . , t n ) ∈ St(σ) then f (t 1 , . . . , t n ) ∈ D, • if t ∈ D, t ∈ St(σ), t = E2 t , then t ∈ D,
• if there is a root reduction s The decision procedure is based on the following reduction lemma, using the facts that the completion is computable and the deduction problem is decidable in the empty equational theory.

Lemma 2. Let E = R 1 ∪ E 2 where R 1 is any subterm E 2 -convergent
TRS and E 2 is any shallow permutative theory. For any normalized frame φ and any normalized term t, we have that φ E t if and only if φ * t.

Static Equivalence. The decision procedure for the static equivalence is based on the computation of small equalities bounded by the size of R 1 .

Definition 5. Let φ = ν ñ.σ be a normalized frame. The set Eq(φ) is the set of equalities

tζ φ = t ζ φ such that (tζ φ )σ = E (t ζ φ )σ where t, t are Σ-terms, (f n(t) ∪ f n(t )) ∩ ñ = ∅, |t|, |t | ≤ |R 1 |.
Given any frame ψ = ν ñ.τ , the fact that tτ = E t τ for any t = t ∈ Eq(φ) is denoted by ψ |= Eq(φ).

To get a decision procedure, it remains to show that checking small equalities defined by Eq are sufficient to prove the static equivalence of the two input frames. Note that the check of each of these equalities is effective since the E-equality is decidable.

Lemma 3. Let E = R 1 ∪ E 2 where R 1 is any subterm E 2 -convergent
TRS and E 2 is any shallow permutative theory. For any normalized frames φ and ψ, we have that φ ≈ E ψ iff ψ |= Eq(φ) and φ |= Eq(ψ).

Main result. According to the above reduction lemmas, we get the following result.

Theorem 1. Let E = R 1 ∪ E 2
where R 1 is any subterm E 2 -convergent TRS and E 2 is any shallow permutative theory. Then, deduction and static equivalence are decidable in E.

To prove both reduction lemmas (Lemma 2 and Lemma 3) and so Theorem 1, we reuse the same approach as in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] by applying two technical lemmas.

The first lemma in the appendix of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] can be generalized as follows.

Lemma 4. Let E = R 1 ∪E 2 where R 1 is any subterm E 2 -convergent TRS and E 2 is any shallow permutative theory. For any terms s and t satisfying the name restriction, if sφ * = E2 tφ * and ψ |= Eq(φ) then (sζ φ )ψ = E (tζ φ )ψ.

Then, the second lemma in the appendix of [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] is generalized in the following way.

Lemma 5. Let E = R 1 ∪E 2 where R 1 is any subterm E 2 -convergent TRS and E 2 is any shallow permutative theory. For any term s satisfying the name restriction and for any term t such that sφ * → R1,E2 t, there exists a term u satisfying the name restriction such that t = E2 uφ * and for any frame ψ such that ψ |= Eq(φ), (sζ φ )ψ = E (uζ φ )ψ.

The proofs of Lemma 4 and Lemma 5 can be found in [START_REF] Erbatur | Computing knowledge in equational extensions of subterm convergent theories[END_REF]. The assumption that E 2 is shallow permutative allows us to get simple proofs.

We are working on generalizing Theorem 1 to syntactic permutative theories E 2 like for instance Associativity-Commutativity. In this general case, the related reduction lemmas for the deduction problem and the static equivalence should be more complicated to express. Indeed, we may have to integrate a deduction procedure modulo E 2 in the construction of the completion, and a static equivalence procedure modulo E 2 to get a reduction lemma for static equivalence in R 1 ∪ E 2 .

Related Work and Conclusion

The intruder deduction problem corresponds to the general cap problem studied in [START_REF] Siva Anantharaman | Intruders with caps[END_REF]. Among other results, it is shown in [START_REF] Siva Anantharaman | Intruders with caps[END_REF] that the general cap problem is in NP for dwindling convergent rewrite systems, which are indeed subterm convergent theories. The NP procedure is given by a saturation procedure used to complete the knowledge given by the input frame. In the conclusion of [START_REF] Siva Anantharaman | Intruders with caps[END_REF], the extension to AC-rewrite systems is mentioned as an interesting future work.

Currently we assume in Definition 3 that the Σ 2 -symbols are constructors, i.e., not appearing at the root of the left-hand sides of the rewrite system. However, this appears to be more restrictive than needed. Indeed, it should be possible to remove this restriction and consider a more relaxed definition where the Σ 2 -symbols are not necessarily constructors. This would allow us to solve the deduction and static equivalence problem in a larger class of theories. For example, we could then consider the theory of Abelian Pre-Group (AP G) defined by the following C-convergent T RS: R AP G = {x * e → x, x * i(x) → e, i(i(x)) → x, i(e) → e} where C = {x * y = y * x}. In [START_REF] Yang | Theories of homomorphic encryption, unification, and the finite variant property[END_REF], AP G = R AP G ∪ C was considered as an approximation to deal with unification in homomorphic encryption over Abelian groups. Theorem 1 would then allow us to also solve the problems of deduction and static-equivalence in AP G.

The next step of our work is to go beyond the class of shallow permutative theories, in order to take into account a larger class including AC. Due to the potential interest of AC in protocol analysis, it is useful to be able to handle some AC-rewrite systems and to study the AC-extension of saturation procedures that have been developed for the intruder deduction problem, the static equivalence [START_REF] Baudet | YAPA: A generic tool for computing intruder knowledge[END_REF], and the static inclusion [START_REF] Gero | Deciding Static Inclusion for Delta-strong and Omega Delta-strong Intruder Theories: Applications to Cryptographic Protocol Analysis[END_REF].

Another challenging problem is to investigate the equational extension of the combination procedure developed in [START_REF] Erbatur | Notions of knowledge in combinations of theories sharing constructors[END_REF] for the deduction and the static equivalence in unions of theories sharing absolutely free constructors. This would permit us to consider shared AC-constructors.

  [r] → R1,E2 t where |s| ≤ |R 1 |, f n(s) ∩ ñ = ∅, r ∈ D and t ∈ St(σ), then t ∈ D. Let σ * = σ{χ u → u | u ∈ D\Ran(σ)} where χ u is a fresh variable. The frame φ * = ν ñ.σ * is called the completion of φ with respect to R 1 . The recipe substitution of φ is ζ φ = {χ u → ζ u | u ∈ D\Ran(σ)} where ζ u denotes an arbitrary recipe of u w.r.t. φ.

  x m are pairwise disjoint variables This definition is well-founded since E 2 is permutative. There exists a mutation-based E 2matching algorithm[START_REF] Erbatur | Unification and matching in hierarchical combinations of syntactic theories[END_REF] since E 2 is syntactic, and so St(t) is computable.

For a set of terms T , St(T ) = t∈T St(t), and for a substitution σ, St(σ) = St(Ran(σ)).

Proposition 1. For any terms t, t , t = E2 t implies St(t) = St(t ), and for any position p in t, St(t| p ) ⊆ St(t).

Acknowledgments: We would like to thank Véronique Cortier for helpful comments and discussions.

* This work has received funding from the European Research Council (ERC) under the H2020 research and innovation program (grant agreement No 645865-SPOOC).


Miren Illarramendi
email: millarramendi@mondragon.edu

Eskola Mondragon Goi

S Politeknikoa

Coop Mondragon

Leire Etxeberria
email: letxeberria@mondragon.edu

Mondragon Goi

Eskola Politeknikoa

S Coop

Rd Xabier Elkorobarrutia
email: xelkorobarrutia@mondragon.edu

Models adaptation at runtime: enhancing the safety of software systems in uncertain scenarios

In current industrial environments, the software of embedded systems have to cope with the increasing complexity, uncertain scenarios and safety requirements at runtime. One approach to managing these requirements is having the software components information in model terms at runtime (models@run.time). Adaptation of models at runtime is one of the challenges to enhance the safety level in uncertain scenarios.

I. INTRODUCTION

An embedded system is a self-contained system that incorporates elements of control logic and real-world interaction. The UML State Machine is a powerful formalism to model the logical behaviour of these types of systems, and in Model-Driven Engineering (MDE) we can generate code automatically from these models.

MDE aims to overcome the complexity of software construction by allowing developers to work at the high-level models of software systems instead of low-level codes [START_REF] Elkorobarrutia | Model-driven software evolution: A research agenda[END_REF]. However, determining and evaluating the runtime behaviour and performance of models of embedded systems using commercial MDE tools is a challenging task. Such tools provide little support to observe at model-level the execution of the code generated from the model, and to collect the runtime information necessary to, for example, check whether defined constraints are met or not [START_REF] Ahmadi | Runtime monitoring of a rover: Mde research with open source software and low-cost hardware[END_REF].

One approach to managing these requirements is having the software components information in model terms at runtime (models@run.time). Work on models@run.time seeks to extend the applicability of models produced in MDE approaches to the runtime environment. Having the model at runtime is the first step towards the runtime verification.

Runtime verification can be performed using the information of model elements (current state, event, next state,etc.) of the UML-SM model of the software component under study. This enables using a common language to design and verify at runtime the software components. Besides, UML-SM is commonly used in industry, thereby avoiding the cost of learning formal languages.

In the next sections, we present a model-driven approach to automatically generate UML-SM code with the ability to provide information of the software component in terms of model elements at runtime and the possibility to adapt this model at runtime when an uncertain or hazard scenario is detected.

II. CRESCO FRAMEWORK

Figure 1 shows the workflow of the approach. First, the behaviour of the components is modelled using UML-SMs by Papyrus [START_REF][END_REF] and the states to be observable at runtime are annotated using the observability profile. This first step is performed by the designer. Once the designer has specified the behaviour of the component, the RESCO model-driven framework will add all the needed infrastructure to allow having the state machine model at runtime. This will be transparent for the designer.

Having these software components with introspection ability, we can design a solution that enables the developers Figure 2 shows the overall architecture of the Runtime Verification solution. In this architecture, on the one hand, we have a software component based system which is compound by an EventReceiver, a software controller designed by UML-SM models, sensors and actuators. On the other hand, we have another execution environment which acts as a safety bag called "Runtime Verification Module" (RVM).

The sensor's events go to the EventReceiver and it performs a preprocessing to check the received events and send them to the dispatcher of the state machine based software components. The dispatcher analyzes the current status of the software component and calculates if a transition to a new state has to be performed.

Additionally, in a reception of an event in an observed state, this information is sent to the Runtime Verification Module by the Observer of the software component. The ObserverReceiver element receives this information and sends it to the RuntimeChecker to check if it is in a safe scenario or not.

When the Runtime Checker checks the information, if the software component is in a safe scenario, it sends an acknowledgment event to the EventReceiver of the software component. The latter performs the corresponding transition and, when needed, it updates output signals to be sent to the actuator. The system continues working in a normal mode. If the RuntimeChecker detects an unsafe scenario the RVM starts the safeModeProcess to change the software component to a safeMode operation mode and it sends the corresponding error event to the EventReceiver of the software-component based system. The software component updates the actuators based on the safeModeProcess indications. This last process is application-specific and has to be defined by the safety engineer.This process could be called as runtime adaptation but in this case this model adaptation was designed at development phase.

III. FUTURE WORKING LINES AND CONCLUSIONS

In [START_REF] Abmann | A reference architecture and roadmap for models@run.time systems[END_REF] they describe open research challenges for models@run.time. Tools for MDE approach, uncertainty management and safety assurance at runtime are some of the open challenges. Our solution is focused on solving the safety assurance and uncertainty management at runtime.

The presented solution manages uncertain or hazardous situations adapting the current model to a predefined safeMode model at runtime. As future work, dynamic runtime model adaptation will be analized. In [START_REF] Trapp | Safety assurance of open adaptive systems a survey[END_REF] they analized which is the current status of the safety assurance of Open Adaptive Systems. They conclude that there are not V&V at Runtime approaches that follows the Models@Runtime approach.

The next step of our research is focused on filling this gap. For that, our approach will be based on deep learning approach to generate new models at runtime. In addition, in order to assure that the suggested dynamic model adaptations are safe, we will need MDE based runtime testing tools. In [START_REF] Helle | Testing of autonomous systemschallenges and current state-of-the-art[END_REF], they suggest a list of "things to do" to test autonomous systems. Some of them, such as the Use of Models, Test Continuously and Virtually and Think Ahead, are on our future research lines.

Fig. 1 .

 1 Fig. 1. Model-driven workflow

Fig. 2 .

 2 Fig. 2. Overall architecture of the Runtime Verification solution scenario.

TABLE I

 I generate software systems able to check their software components in model terms at runtime.For runtime checking, some decisions must be taken about what to observe. TableIprovides the information available from the CRESCO SW components at runtime.

		CRESCO OBSERVED DATA
	Data	Description
	Component Name Identification of the current component
	Current State	Identification of the current state
	Next State	Identification of the next/target state
	Father State	Identification of the father state
	Event Id	Identification of the current event

to

ACKNOWLEDGMENT

The project has been developed by the Embedded System Group of MGEP and supported by the Department of Education, Universities and Research of the Basque Government under the projects Ikerketa Taldeak (Grupo de Sistemas Embebidos) and by the European H2020 research and innovation programme, ECSEL Joint Undertaking, and National Funding Authorities from 19 involved countries under the project Productive 4.0 with grant agreement no. GAP-737459 -999978918.