Rudyar Cortés
email: [rudyar.cortes@lip6.fr

Xavier Bonnaire
email: xavier.bonnaire@inf.utfsm.cl

Olivier Marin

Luciana Arantes
email: luciana.arantes@lip6.fr

Pierre Sens
email: pierre.sens]@lip6.fr

GeoTrie: A Scalable Architecture for Location-Temporal Range Queries over Massive GeoTagged Data Sets

Keywords: Big Location Data, Location-Temporal Range Queries, Scalability

The proliferation of GPS-enabled devices leads to the massive generation of geotagged data sets recently known as Big Location Data. It allows users to explore and analyse data in space and time, and requires an architecture that scales with the insertions and location-temporal queries workload from thousands to millions of users. Most large scale key-value data storage solutions only provide a single one-dimensional index which does not natively support efficient multidimensional queries. In this paper, we propose GeoTrie, a scalable architecture built by coalescing any number of machines organized on top of a Distributed Hash Table . The key idea of our approach is to provide a distributed global index which scales with the number of nodes and provides natural load balancing for insertions and location-temporal range queries. We assess our solution using the largest public multimedia data set released by Yahoo! which includes millions of geotagged multimedia files.

I. INTRODUCTION

An ever increasing number of GPS-enabled devices such as smartphone and cameras generate geotagged data. On a daily basis, people leave traces of their activities involving mobile applications, cars, unmanned aircraft vehicles (UAVs), ships, airplanes, and IoT devices. These activities produce massive flows of data which cannot be acquired, managed, and processed by traditional centralized solutions within a tolerable timeframe. The time and geographic analysis of such data can be crucial for life saving efforts by helping to locate a missing child, or for security purposes allowing to know which smartphone and therefore who was present in a given area and during a specific event. An emergent field of research, known as Big Location Data [START_REF] Pelekis | The case of big mobility data[END_REF]- [START_REF] Ranga | Spatiotemporal data mining in the era of big spatial data: algorithms and applications[END_REF], addresses this issue.

The essential characteristic of Big Location Data is that it associates every data with meta-data which includes a geotag and a timestamp. Location-temporal range queries [START_REF] Gaede | Multidimensional access methods[END_REF] represent a major challenge for data extraction, exploration and analysis, within both a geographic area and a time window.

Popular multimedia services such as Instagram1 , Flickr2 or Twitter 3 are examples of already existing applications that generate continuous and massive flows of data, enriched with meta-data including geotags and timestamps.

Other services which do not rely on user interaction, like automatic smartphones location or smart cities, can generate meta-data on an even larger scale. Allowing millions of users to explore these data sets could help get more insight about what happens in particular geographic areas within given timeframes. For instance, people who attended a concert between 20:00 p.m. and 01:00 a.m. may want to review public pictures and comments from people who attended the same concert. The concert manager may want to acquire more feedback about the overall concert experience by analyzing pictures, comments and tags. Or people might want to verify whether the referee of a football match missed a foul by catching multiple amateur videos and pictures of the action.

The main challenge presented by such services is to guarantee scalability, fault tolerance, and load balancing for a high number of concurrent insertions and location-temporal range queries. Relational databases cannot reach such scales: their response time significantly increases when concurrent insertions and queries have to cover billions of objects. Other approaches that rely on a centralized global index [START_REF] Eldawy | Spatialhadoop: A mapreduce framework for spatial data[END_REF]- [START_REF] Randall T Whitman | Spatial indexing and analytics on hadoop[END_REF] contend with a bottleneck. More recent approaches use spacefilling curves [START_REF] Samet | Foundations of multidimensional and metric data structures[END_REF] in order to collapse the latitude and longitude coordinates into a one-dimensional index and distribute it over multiple nodes [START_REF] Nishimura | Md-hbase: a scalable multi-dimensional data infrastructure for location aware services[END_REF]- [START_REF] Lee | Efficient spatial query processing for big data[END_REF]. Although they allow scalable location-temporal query processing, the curse of dimensionality [START_REF] Samet | Foundations of multidimensional and metric data structures[END_REF] introduces several processing overheads which impact the query response time.

In this paper, we present a scalable architecture for location-temporal range queries. The main component of the architecture is a distributed multidimensional global index which supports location-temporal range querying on a large scale, and provides natural insertion and query load balancing.

The main contributions of this paper are:

• An approach to introduce location-temporal data locality in a fully decentralized system such as a distributed hash table. This approach is based on a multidimensional distributed index which maps latitude, longitude, timestamp tuples into a distributed prefix octree, thus efficiently filtering false positives while providing fault tolerance and load balancing for internetscale applications. • A theoretical evaluation of our solution, which shows that its message complexity for insertions and range queries is logarithmic with respect to the number N of nodes involved. • A practical evaluation, which shows that our solution alleviates the bottleneck on the root node during insertions and range queries. This property has an impact on the query response time. For instance, queries which avoid the root node presents an average query response time up to 1.9x faster than queries which starts at the root level.

The rest of this paper is organized as follows. We detail our solution in Section II, and then evaluate it in Section III using a large public multimedia dataset from Yahoo!. We give an overview of the related work in Section IV, before concluding in Section V.

II. SYSTEM DESIGN

We aim to propose a scalable architecture for indexing and querying meta-data extracted from geotagged data sets.

We choose to work on top of a distributed hash table (DHT) such as Pastry [START_REF] Rowstron | Pastry: Scalable, decentralized object location, and routing for large-scale peer-to-peer systems[END_REF] or Chord [START_REF] Stoica | Chord: A scalable peer-to-peer lookup service for internet applications[END_REF] because it provides a strong basis for scalable solutions as opposed to centralized server architectures. DHTs provide an overlay with properties such as self-organisation, scalability to millions of nodes (usually routing has a message complexity of O(log(N )), where N is the number of nodes) and dependability mechanisms via replication. However, a DHT by itself cannot constitute a satisfactory solution for scalable location-temporal data storage and retrieval because the hash function usually destroys data locality for the sake of load balancing.

The proposed architecture must create data locality over DHTs based on three core dimensions: latitude, longitude and timestamp. We assume that every meta-data entry references data stored on an external storage service. We intent for our architecture to achieve the following properties. Fig. 1: Latitude mapping example. The latitude value 24.550558 is mapped to the binary string T lat = 1010001011101010100101011101101

• Query load balance: Meta-data insertions and locationtemporal range queries must be distributed in the architecture in order to avoid a single bottleneck. • High Availability: The architecture must tolerate node failures. Geotrie builds location-temporal data locality over a DHT following two main steps: mapping and indexing. The mapping step associates every (latitude,longitude,timestamp) coordinate with a tuple key T k = (T lat , T lon , T t ), where every coordinate of T k is a 32-bit word. The indexing step inserts every tuple key T k in a fully distributed prefix octree which allows efficient location-temporal range queries.

A. Mapping

Let lat ∈ [-90, 90], lon ∈ [-180, 180], and t ∈ [0, 2 32 -1] be the latitude, longitude and timestamp parameters of a given geotagged object. The timestamp coordinate corresponds to the Unix epoch timestamp. We map every coordinate to the multidimensional tuple key T k = (T lat , T lon , T t ), where every tuple belongs to the same domain {0, 1} 32 (i.e, binary string of 32 bits per coordinate).

Geotrie performs domain partitioning for all the coordinates as follows. First, the space domain [a, b] of every coordinate is divided in two buckets D lef t = [a, (a + b)/2] and D right =](a + b)/2, b]. A bit value of 0 represents a point that belongs to the left sub domain, while a bit value of 1 positions it in the right subdomain. This process continues recursively until all D = 32 bits are set. For instance, the first bit of latitude -45 is 0 because it belongs to the first left subdomain [-90,0]. This mapping function reaches its lower bound at latitude value lat = -90 represented as the identifier {0} 32 , and its upper bound at lat = 90 represented as the identifier {1} 32 . Longitudes incur the same process, with the lower bound at lon = -180 and the upper bound at lon = 180. Every tuple T k encloses coordinates into a location-temporal cell which covers an area of 0.46 cm × 0.93 cm at the equator, and ensures a one second time precision. It also induces the following properties. That is, all keys with the same prefix necessarily belong to the single and same area represented by this prefix.

For instance, all keys that share the same prefix key (00,00,00) belong to the interval covered by this prefix. Note that the converse is not true; for instance 011 and 100 are adjacent but they do not share a common prefix.

B. Indexing

The GeoTrie structure exploits both properties presented above. It indexes every tuple key T k = (T lat , T lon , T t ) into a distributed prefix octree-like indexing structure built on top of a DHT.

Every GeoTrie node holds a label l, a state s, and the range it covers. The label l is a prefix of T k and the state s can either be leaf node, internal node, or external node. Only leaf nodes store data; internal nodes stand on the path to leaf nodes that do hold data, while external nodes stand outside any such path. A DHT node declares itself to be an external node for a label l, when it receives a query asking for a non existing label l on its local data structure. The range covered by a GeoTrie node is locally computed by using its label l and the recursive prefix domain partition property presented above. Furthermore, every internal node stores links to its direct children nodes and the range they cover.

Every GeoTrie node is assigned to the DHT node whose identifier in the ring is closest to the key k = Hash(l).

Upon start-up, GeoTrie consists of a single root node with label l = ( * , * , * ) and leaf node state. When a node becomes full, GeoTrie scales out by switching it to internal and dispatching its load onto eight new leaf nodes created via recursive prefix domain partitioning.

Figure 2 shows a representation of the GeoTrie data structure for tuple keys of size D = 2 bits. GeoTrie can take advantage of any replication mechanism used by DHTs in order to provide fault tolerance. For instance, in Pastry [START_REF] Rowstron | Pastry: Scalable, decentralized object location, and routing for large-scale peer-to-peer systems[END_REF] Geotrie can use the leaf set in order to replicate and maintain the state of every Geotrie node.

Insertions and deletions. Storing and deleting an object with key T k consists first in locating the leaf node whose label is prefix of T k , and then in carrying out the insertion or deletion operation directly on this node. For instance in Figure 2, tuple key T k1 = (00, 00, 00) is stored on the leaf node with label l 1 = (00, 00, 00) and tuple key T k2 = (10, 10, 10) is stored on the leaf node with label l 2 = (1, 1, 1). Algorithm 2 presents a pseudocode of the insertion operation; it uses the locateLeaf procedure detailed in Algorithm 1. locateLeaf receives a tuple key T k as input and returns the leaf node whose label is prefix of T k . It does so by performing a binary search over different possible prefixes of T k until a node with state leaf node is reached. For every tuple key T k , there are exactly D possible prefix labels plus the root node, and only one them can designate a leaf node. The client starts by sending a lookup message to a label prefix of T k of size D/2 (i.e, the middle of the space of possible candidates). This label is computed by extracting the first D/2 bits of every coordinate. If the state of this node is external, it means that the target leaf node keeps a label of shorter prefixes. In this case, the binary search cuts the space to prefixes of higher size D/2 -1 and it propagates the lookup to shorter prefixes. Instead, if the target node is an internal node it means that the leaf node keeps a longer prefix. It cuts the space to a lower prefix of size D/2 + 1 and propagates the search down GeoTrie. This process continues recursively and ends upon reaching a leaf node whose label is prefix of T k . If the locateLeaf algorithm fails to return a leaf node due to index maintenance, the client must retry the insertion at a later time. This binary search procedure benefits of the prefix property of GeoTrie which allows queries to start at any node, and thus prevents the root node from becoming a bottleneck.

Index maintenance. GeoTrie provides two index maintenance operations: split and merge. The split operation occurs when a leaf node stores B keys, where B is a system parameter. An overloaded leaf node scales out its load by creating eight new children nodes via recursive domain partitioning. The dispatch of data follows the prefix rule: a data entry with index T k gets transferred to the new leaf node whose label l is prefix of T k ). After transferring all its data, the split node The merge operation is the opposite to the split operation. GeoTrie triggers the merge operation on a group of eight leaf nodes which share the same internal node as parent when the sum of their storage loads becomes less than B/8 objects. When this happens the internal node sends a merge message to all its leaf node children, thus requesting they transfer back all their stored data. Upon transfer completion, all children leaf nodes detach from the prefix tree structure and the parent switches its state from internal node to leaf node. Typical applications generate far more insertions than deletions, so we expect a low proportion of merge operations compared to split operations.

Input: (∆Lat b , ∆Lon b , ∆t b ) Output: M eta -data pref ixLat = commonP ref ix(∆Lat b ); pref ixLon = commonP ref ix(∆Lon b ); pref ixT ime = commonP ref ix(∆t b ); //
Location-temporal range queries. A location-temporal range query is represented as a three dimensional range query as presented in equation 1.

∆Lat = [lat1, lat 2 ], lat 1 , lat 2 ∈ [-90, 90] ∆Lon = [lon 1 , lon 2 ], lon 1 , lon 2 ∈ [-180, 180] ∆t = [t i , t f ], t i , t f ∈ [0, 2 32 -1] (1)
This query is resolved as follows. First, the sender node uses the mapping function defined above in order to translate every coordinate constraint (∆Lat, ∆Lon, ∆t) into binary strings belonging to the domain {0, 1} 32 as presented in equation 2.

∆Lat b = [lat 32 1 ,
Then, it computes the common prefix label of minimum common size for every coordinate constraint and it forwards the query to the node which covers this label. For instance, query Q which combines constraints ∆Lat b = [00..., 01...], ∆Lon b = [10..., 11...], and ∆t b = [110..., 110...] has a common prefix label of every coordinate (0, [START_REF] Pelekis | The case of big mobility data[END_REF][START_REF] Lee | Efficient spatial query processing for big data[END_REF]. This common prefix label has not a common size because the time coordinate is longer than the others. Thus, this common prefix is converted to a label of minimum common size l Q = (0, 1, 1) which represents a label of GeoTrie. This label covers all data which is inside the interval of Q. If there is not common prefix, the query must start from the root node labeled l = ( * , * , * ). Algorithm 3 presents a pseudocode for this procedure.

Depending on the state s of the node which receives the query, we identify three cases. (i) If the node is an internal node, it uses the forwardRequest function in order to recursively forward the query onward to the leaf nodes whose location-temporal range intersects that of the query interval. (ii) If the node is a leaf node, it is the only node that covers the required location-temporal range and returns the objects that satisfy the query. (iii) If the node is an external node, it follows that the common prefix is a label which does not yet exist in the prefix tree (i.e, the query arrived to a DHT node which does not hold this label). In this case, the query is necessarily covered by a single leaf node. in order to find this particular leaf node, the client node then starts the LocateLeaf algorithm from the label of the external node.

III. EVALUATION

This section presents a theoretical and an experimental evaluation of GeoTrie. The theoretical evaluation assesses the scalability of the solution in terms of the message complexity for insertions and range queries. An extensive experimental evaluation studies the load balancing and the performance of GeoTrie in terms of the query response time. We chose to conduct our experimental evaluation with a real dataset: the Yahoo Flickr Creative Commons (YFCC) dataset [START_REF] Thomee | Yfcc100m: The new data in multimedia research[END_REF] released by Yahoo! It comprises 48, 469, 177 geotagged multimedia files (photos and videos).

A. Overview

This section presents a simulation-based assessment of GeoTrie to measure its performance, with a large scale real world dataset from Yahoo!

We implemented GeoTrie on top of FreePastry [START_REF] Druschel | Software available[END_REF], an open-source DHT implementation. In our experiments, we deployed N = 1, 000 DHT nodes. Every leaf node stores at most B = 10, 000 keys. We assume that DHT nodes are 3a shows the observed distribution of latencies on the DHT nodes during our experiments. 1) Query set: In order to assess the performance of GeoTrie under different range query spans, we generated six query sets (QS) which cover different geospatial bounding box sizes and timespans as follows. First, we randomly picked 1, 000 tuples t k = (latitude, longitude, timestamp) from the dataset. Then, for every query set and for every tuple, we generated a query for a geospatial bounding box which encloses a M × M kilometres square with a time interval of H hours with centre in t k .

Table II presents the size of M and H we chose for this evaluation and Table III presents the distribution of the data items that match every query set. These queries represent different bounding box sizes and timespans. For instance, query sets QS1 and QS2 represent highly selective queries. They target bounding boxes of 2 × 2 km 2 and timespans of 1 and 48 hours respectively. Query sets QS3 and QS4 target bigger bounding boxes of 200 × 200 km 2 , with respective timespans of 1 and 48 hours. The query set QS5 targets all the space domain with a timespan of one hour. Finally, the query set QS6 targets all the time domain with a bounding box of two kilometres side size. Query sets QS5 and QS6 are specific in that the former covers the entire geospatial domain and the latter covers the entire temporal domain. Therefore, they both always start at the root node because of the absence of a common prefix. We believe that these combinations of queries represent a rich workload to assess the query load balance and performance of GeoTrie.

B. Data insertions 1) Message Complexity:

Let N be the number of nodes in the DHT, n the number of keys to be indexed, and D the number of bits used to represent the data domain {0, 1} D of every coordinate of the tuple key T k . The insertion/deletion of a data object identified by T k involves a binary lookup in order to find the leaf node whose label is a prefix of T k . Equation 3 presents the message complexity in terms of the number of DHT lookup messages generated by a single insertion/deletion operation. Note that the message complexity of every DHT lookup is O(log(N ). So the total number of messages generated by a single insertion/deletion operation is given by equation 4.

C ins/del (D) = O(log(D)) (3)
C ins/del total = O(log(D)) × O(log(N )) (4)
The message complexity of insertions and deletions on GeoTrie does not depend on the number of objects n. A balanced tree index built on top of a DHT requires O(log(n)) DHT lookups. Via binary searches on a trie whose height cannot exceed 32, GeoTrie outperforms a balanced tree for large values of n. For instance, indexing a new entry among 50 million keys of size D = 32 bits requires about 25 DHT lookups with a tree, while GeoTrie does the job in about 5 DHT lookups. 2) Insertion time: In this experiment, we indexed all the meta-data of 48, 469, 177 geotagged multimedia files extracted from the YFCC dataset [START_REF] Thomee | Yfcc100m: The new data in multimedia research[END_REF] at a rate of 1, 000 items per second. At every insertion, a DHT node is chosen randomly in order to perform the operation. Then, we measured the insertion time as the time elapsed between the moment the client node starts the insertion process until the moment the leaf node successfully stores the item.

Table V presents the overall distribution of insertion latencies. Most of the latencies are concentrated between 1.8 and 3.3 seconds with a median of 2.84 seconds. The insertion time depends of the size of the prefix label of the target leaf node. Some insertions can directly arrive to the target leaf node through the binary search algorithm presented in section II. Others insertions require more messages to locate the target leaf node. In order to understand the behaviour of the binary search we measured the distribution of the number of DHT lookups in the insertion process. C. Location-temporal range queries 1) Message Complexity: A location-temporal query on GeoTrie first reaches the node which maintains the common prefix label of minimum common size, and then branches out in parallel down the tree until it reaches all leaf nodes. Equation 5 computes the number of messages for this operation.

O(log(N )) ≤ C range-query ≤ O(log(N )) + D + 1 (5)
The lower bound occurs when the query arrives directly to a single leaf node which covers the interval, and the upper bound occurs when there is no common prefix of minimum size. In the worst case, the query arrives at the root node labeled l = ( * , * , * ) and traverses the whole tree in parallel through a maximum of D + 1 levels (the root node plus the maximum prefix size D=32). Note that the global implicit knowledge introduced by GeoTrie allows to reach the query subspace directly when it does not include the root node. Unlike queries that cover large geographic areas and timespans, queries which target small geographic areas and timespan share a larger common prefix of minimum size, and therefore directly arrive to higher levels of GeoTrie (i.e., close to the leaves). Indexes relying on a balanced tree usually start queries from the root node, and thus induces bottlenecks.

2) Range query performance: In this experiment, we study queries whose prefix maps to any other node than the root node. More specifically, we assess their impact on the query response time under a workload composed of concurrent range queries. In order to conduct this experiment, we generated a workload of 1, 000 queries per second for every QS1 to QS5. Every query originates from a DHT node chosen at random. It consists in counting the number of items inside the location-temporal range.

Figure 3b and table VII presents the query response time measured as the time elapsed between emission of the query and the latest reception of results from all the leaf nodes that store data relevant to this query. Only about 1% of the query response time corresponds to processing time (i.e, the time it takes a leaf node to filter-out all the data outside the query interval). The remaining 99% of the time corresponds to communication latency. Indeed, in our experiment the metadata is stored in memory, and therefore the local processing cost of a query over a single leaf node is much lower than the network latency cost. As expected, queries that span a shorter space present a lower query response time than queries that span a larger space. For instance, the average query response time is 1.9x slower for queries of QS3 than for queries of QS5. Indeed, we tailored queries in this experiment so that they can avoid the root node. Our results show that Geotrie thus allows to alleviate a potential bottleneck on the root node, and this has a considerable impact on the query response time.

In order to understand how queries are distributed among the GeoTrie structure we measured the GeoTrie level starting point (SP) for QS1 and QS3. We exclude both QS5 and QS6 because by construction they always start at the root node. Table VIII presents our results. Only 0.3% of queries of QS1 (3 out of 1,000) starts at the root node, and 75% of the total amount of queries starts at a level greater or equal than 5. In the case of QS3, 8.3% of the queries (83 out of 1,000) started at the root node and the 75% of the queries started at a level greater or equal than 3. QS3 queries target bigger areas, and therefore match shorter common prefixes in the trie structure. Hadoop-based solutions such as SpatialHadoop [START_REF] Eldawy | Spatialhadoop: A mapreduce framework for spatial data[END_REF], Hadoop GIS [START_REF] Aji | Hadoop gis: a high performance spatial data warehousing system over mapreduce[END_REF], and ESRI Tools for Hadoop [START_REF] Randall T Whitman | Spatial indexing and analytics on hadoop[END_REF], extend the traditional Hadoop architecture [START_REF] White | Hadoop: the definitive guide: the definitive guide[END_REF] with spatial indexing structures such as R-Trees [START_REF] Guttman | R-trees: A dynamic index structure for spatial searching[END_REF] or Quad-Trees [START_REF] Finkel | Quad trees a data structure for retrieval on composite keys[END_REF] in order to avoid a scan of the whole dataset when performing spatial analysis. These approaches employ a two-layer architecture that combines a global index maintained on a central server with multiple local indexes. For instance, SpatialHadoop [START_REF] Eldawy | Spatialhadoop: A mapreduce framework for spatial data[END_REF] builds spatial indexing structures over HDFS [START_REF] Aji | Hadoop gis: a high performance spatial data warehousing system over mapreduce[END_REF] in order to add spatial support for MapReduce tasks. However, these solutions are ill-suited for concurrent insertions and locationtemporal queries because (i) the global index structure on a single node is prone to become a bottleneck, and (ii) they are designed for batch processing of large tasks. Unlike these solutions, GeoTrie constitutes a large scale global locationtemporal index which provides random access and fault tolerance for concurrent insertions and location-temporal queries.

Resilient Distributed Dataset (RDD) based solutions such as Spatial Spark [START_REF] You | Large-scale spatial join query processing in cloud[END_REF] and GeoTrellis4 extend traditional RDD solutions such as Spark [START_REF] Zaharia | Spark: cluster computing with working sets[END_REF] in order to support big location data. Similarly to Hadoop-based solutions, these systems are designed for batch processing and do not target online processing.

Key-value store-based solutions such as MD-Hbase [START_REF] Nishimura | Md-hbase: a scalable multi-dimensional data infrastructure for location aware services[END_REF], MongoDB [START_REF] Chodorow | MongoDB: the definitive guide[END_REF], ElasticSearch [START_REF] Gormley | Elasticsearch: The Definitive Guide[END_REF], and GeoMesa [START_REF] Fox | Spatio-temporal indexing in non-relational distributed databases[END_REF] require linearization techniques such as space-filling curves [START_REF] Samet | Foundations of multidimensional and metric data structures[END_REF] in order to collapse several dimensions into a single onedimensional index and to support multi-dimensional queries. Then, the multidimensional query can be reduce to a single dimensional space. However, space-filling curves [START_REF] Samet | Foundations of multidimensional and metric data structures[END_REF] loosely preserve data locality and introduce several I/O overheads when the number of dimensions increase due to the curse of dimensionality [START_REF] Samet | Foundations of multidimensional and metric data structures[END_REF]. These overheads impacts negatively the query response time. Unlike these solutions, GeoTrie follows a multidimensional approach which drastically reduces this overhead.

DHT-based solutions can be classified into two main groups: (i) extensions of traditional indexing structures such as B-Trees, Prefix Trees, R-Trees, QuadTrees, and KDtrees to DHTs [START_REF] Sriram Ramabhadran | Prefix hash tree: An indexing data structure over distributed hash tables[END_REF]- [START_REF] Cortés | A scalable architecture for spatio-temporal range queries over big location data[END_REF], and (ii) overlay-dependent solutions [START_REF] Wang | Indexing multi-dimensional data in a cloud system[END_REF]- [START_REF] Tang | mlight: indexing multi-dimensional data over dhts[END_REF]. Compared to the solutions of the first group, GeoTrie performs domain partitioning to prevent bottlenecks on the root node, and introduces global knowledge about the tree structure to balance the load of insertions and range queries. To the best of our knowledge, the only structure which performs domain partitioning over a DHT is the Prefix Hash Tree (PHT) [START_REF] Sriram Ramabhadran | Prefix hash tree: An indexing data structure over distributed hash tables[END_REF]. PHT can handle multi-dimensional data using linearisation techniques such as z-ordering. As mentioned previously, however, dimensionality reduction with respect to space and time introduces query overheads due to the curse of dimensionality. GeoTrie reduces this overhead because it uses a multidimensional structure and, unlike the solutions of the second group, it is portable to any DHT.

V. CONCLUSION

This paper presents GeoTrie, a scalable architecture for massive geotagged data storage and retrieval built on top of a DHT. Our solution indexes the location and temporal dimensions of every meta-data on a multidimensional distributed structure which scales and balances the load of insertions and range queries. A theoretical analysis of the message complexity of every operation on GeoTrie demonstrates its scalability. An extensive experimental evaluation over a Yahoo! dataset comprising about 48 millions of multimedia files shows that our solution balances the load of insertions and range queries on a large scale. In a configuration involving 1, 000 nodes, queries which avoids the root node presents an average query response time up to 1.9x faster than queries which starts at the root level. This property of GeoTrie allows to alleviate a potential bottleneck on the root node. We are currently working on an extension of our proposal to handle n-dimensional range queries over massive data sets.

Fig

  Fig. 2: GeoTrie Example: Distributed data structure for keys of D=2 bits size

•

  Recursive prefix domain partition. The mapping function presented above recursively partitions every latitude, longitude, and timestamp coordinates into eight Input: Tuple key T k Meta-data m node = LocateLeaf(T k ); node.insert(leafAddr,T k ,m); Algorithm 2: Insertion pseudocode areas represented by prefixes. For instance, the tuple key T k = (0, 0, 0) represents all the latitude,longitude, and timestamp tuples within the interval latitude ([-90, 0]), longitude ([-180, 0]), and timestamp [0, (2 32 -1)/2]). The next subdomain T k = (00, 00, 00) represents the domain latitude ([-90, -45]), longitude ([-180, -90]), and timestamp = ([0, (2 32 -1)/4]), and so on. • Prefix data locality. Shared prefixes imply closeness.

  Fig. 3: Latency among DHT nodes and GeoTrie Performance

  IV. RELATED WORK Large scale architectures to store, query and analyse big location data constitute a fast-growing research topic. Current solutions fall into four groups: (i) Hadoop-based solutions; (ii) Resilient Distributed Dataset (RDD) based solutions; (iii) Keyvalue store-based solutions, and (iv) DHT-based solutions.

  . 2: GeoTrie Example: Distributed data structure for keys of D=2 bits size

	Input: Tuple key T k
	Output: Leaf node
	lower = 0;
	higher = D;
	while lower ≤ higher do
	middle = (lower + higher)/2;
	// Extract the prefix of size middle
	of every coordinate of T k and
	route the message
	node = DHT lookup(T middle (T k ));
	if node is a leaf node then
	return node;
	else
	if node is an internal node then
	lower = middle + 1;
	else
	// node is external node
	higher = middle -1;
	end
	end
	end
	return f ailure;
	Algorithm 1: LocateLeaf pseudocode
	The mapping of the timestamp coordinate follows the same
	principle. It results in the binary representation of the Unix
	epoch. Figure 1 presents an example of the mapping strategy
	for latitude value 24.550558.

  Common prefix of minimum size target = minComPrefix(PrefixLat,PrefixLon,PrefixTime); Location-temporal range query pseudocode changes its state from leaf node to internal node and every child node becomes a new leaf node.

	// If there is not a common prefix
	start from the root node
	if target = (, , , ) then
	target = ( * , * , * );
	end
	node = DHT -lookup(target);
	if node is a leaf node then
	// process the request
	return LocalRequest(∆Lat, ∆Lon, ∆t);
	else
	if node is an internal node then
	// forward the request to the
	children nodes that covers the
	range
	f orwardRequest(children);
	else
	// Node is an external node
	// Locate the leaf node which
	covers all the interval using
	the target label as starting
	point
	node = LocateLeaf (target) // Forward
	the request to this node
	f orwardRequest(node)
	end
	end
	Algorithm 3:

TABLE I :

 I Distribution of latencies among DHT nodes

	Query set (QS) B. Box M × M (km 2 ) Time interval (H)
	1	2 × 2	1
	2	2 × 2	48
	3	200 × 200	1
	4	200 × 200	48
	5	ALL	1
	6	2 × 2	ALL

TABLE II :

 II Location-temporal range query sets distributed worldwide. We used a baseline latency file provided in the FreePastry distribution to generate latencies among DHT nodes. TableIgives the baseline values, while Figure

  3: Latency among DHT nodes and GeoTrie Performance

	Dist.	QS1	QS2	QS3	QS4	QS5	QS6
	Min.	1	1	1	1	60	1
	Quartile 1	6	12	15	95	535	259
	Quartile 2	21	37	36	256	771	1,393
	Quartile 3	56	113	81	612	1,027	9,089
	Max.	5,353	62,333 6,079	77,629	6,694	215,647
	Avg.	50	169	68	555	825	14,008

TABLE III :

 III Distribution of the number of data items that match every query set QS

	Dist.	QS1	QS2	QS3 QS4	QS5	QS6
	Min	1	1	1	1	796	4
	Quartile 1	1	1	5	5	1693	15
	Quartile 2	1	1	9	9	2023	23
	Quartile 3	1	1	14	14	2161	38
	Max	31	82	54	108	2227	284

TABLE IV :

 IV Query cost distribution.

TABLE V :

 V Insertion latency distribution

	# DHT lookups Percentage [%] Min. Time[s]	Avg. Time [s] Max Time [s]
	1	0.05	1 x 10 -3	0.83	1.62
	2	27.79	1 x 10 -3	1.47	3.20
	3	2.01	0.387	2.12	3.90
	4	20.27	0.49	2.71	5.05
	5	49.84	0.82	3.34	6.12
	6	0.04	2.32	3.88	5.76

TABLE VI :

 VI Number of DHT lookups per insertion and its latency distribution

  Table VI presents our results. Since the binary search algorithm is inherently sequential, the number of DHT lookups has a strong impact on the insertion latency. For instance, most insertions (49.84%) require 5 DHT lookups. They present an average latency of 3.34 seconds. Instead, insertions that require 2 lookups (27.79 %) present an

	(QS#) Min	Quartile 1	Quartile 2 Quartile 3	Max Avg
	1	0.21	1.45	1.76	2.06	3.11	1.72
	2	0.09	1.41	1.77	2.05	3.07	1.69
	3	0.01	1.32	1.62	1.97	3.76	1.68
	4	0.15	1.33	1.64	1.97	3.99	1.69
	5	2.47	3.11	3.24	3.35	4.52	3.23
	6	1.34	2.4	2.65	2.90	4.67	2.66

TABLE VII :

 VII Location-temporal range query response time in seconds

	Distribution QS1 SP QS3 SP
	Min	0	0
	Quartile 1	5	3
	Quartile 2	6	5
	Quartile 3	6	5
	Max	12	6

TABLE VIII :

 VIII Distribution of the GeoTrie level starting point for QS1 and QS3 average insertion latency of 1.47 seconds (2.27 times faster).

https://instagram.com

https://www.flickr.com

http://www.twitter.com

• Self-organisation: The architecture must be selforganised. That is, every node must run a local protocol without needing to add a central third party. • Scalable query processing: Meta-data insertions and location-temporal range queries must scale with the number of available nodes in the DHT.

http://geotrellis.io


Burak Ekici
email: burak-ekici@uiowa.edu

Guy Katz
email: guy.katz@nyu.edu

Chantal Keller
email: chantal.keller@lri.fr

Alain Mebsout
email: alain-mebsout@uiowa.edu

Andrew J Reynolds
email: andrew-reynolds@uiowa.edu

Cesare Tinelli
email: cesare-tinelli@uiowa.edu

Final version to appear in: HaTT'16 Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver ZChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.

Introduction

SMTCoq 1 [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] is a tool that allows the Coq [START_REF] Barras | The Coq proof assistant: reference manual[END_REF] proof assistant to communicate with external automatic solvers for Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT). Its twofold goal is to:

• increase the confidence in SAT and SMT solvers: SMTCoq provides an independent and certified checker for SAT and SMT proof witnesses;

• safely increase the level of automation of Coq: SMTCoq provides starting safe tactics to solve a class of Coq goals automatically by calling external solvers and checking their answers (following a skeptical approach).

SMTCoq currently supports the SAT solver ZChaff [START_REF] Yogesh | Zchaff2004: An Efficient SAT Solver[END_REF] and the SMT solver veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF] for the quantifierfree fragment of the combined theory of linear integer arithmetic and equality with uninterpreted functions. For this combined theory, SMTCoq's certificate checker has proved to be as efficient as state-ofthe-art certified checkers [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF][START_REF] Böhme | Fast LCF-Style Proof Reconstruction for Z3[END_REF]. There is a large variety of SAT and SMT solvers, with each solver typically excelling at solving problems in some specific class of propositional or first-order problems. While the SAT and SMT communities have adopted standard languages for expressing input problems (namely the DIMACS standard for SAT and the SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF] standard for SMT), agreeing on a common output language for proof witnesses has proven to be more challenging. Several formats [START_REF] Van Gelder | Producing and verifying extremely large propositional refutations -Have your cake and eat it too[END_REF][START_REF] Stump | SMT proof checking using a logical framework[END_REF][START_REF] Besson | A Flexible Proof Format for SMT: a Proposal[END_REF] have been proposed but none has emerged as a standard yet. Each proof-producing solver currently implements its own variant of these formats. To be able to combine the advantages of multiple SAT and SMT solvers despite the lack of common standards for representing proof certicates, SMTCoq has been designed to be modular along two dimensions:

SMTCoq

• supporting new theories: SMTCoq's main checker is an extendable combination of independent small checkers;

• supporting new solvers: SMTCoq's kernel relies on a generic certificate format that can encode most SAT and SMT reasonings for supported theories; the encoding can be done during a preprocessing phase, which does not need to be certified.

In this abstract, we emphasize the key ideas behind the modularity of SMTCoq, and validate this by reporting on work in progress on the integration of the SMT solver CVC4 [START_REF] Barrett | CVC4[END_REF] and the theory of bit vectors. We simultaneously aim at:

• offering to CVC4 users the possibility to formally check its answers in a trusted environment like Coq;

• bringing the power of a versatile and widely used SMT solver like CVC4 to Coq;

• providing in Coq a decision procedure for bit vectors, a theory widely used, for instance, for verifying circuits or programs using machine integers.

2 The SMTCoq Tool

General Idea

The heart of SMTCoq is a checker for a generic format of certificates (close to the format proposed by Besson et al. [START_REF] Besson | A Flexible Proof Format for SMT: a Proposal[END_REF]), implemented and proved correct inside Coq (see Figure 1a). Taking advantage of Coq's computational capabilities the SMTCoq checker is fully executable, either inside Coq or after extraction to a general-purpose language [START_REF] Letouzey | A New Extraction for Coq[END_REF]. The Coq signature of this checker is the following:

checker : formula → certificate → bool
where the type formula represents the deep embedding in Coq of SMT formulas, and the type certificate represents SMTCoq's format of certificates. The checker's soundness is stated with respect to a translation function from the deep embedding of SMT formulas into Coq terms:

• : formula → bool that interprets every SMT formula into its Coq Boolean counterpart. The correctness of the checker: checker_sound : ∀ f c, checker f c = true → f thus means that, given a formula and a certificate for which the checker answers positively, then the interpretation in Coq of the formula is valid.

The choice of the type of Booleans bool as the codomain of the translation function • , instead of the type of (intuitionistic) propositions Prop, allows us to handle the checking of the classical reasoning made by SMT solvers without adding any axioms. The SSReflect [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF] plugin for Coq can be used to bridge the gap between propositions and Booleans for the theories considered by SMTCoq. The major shortcoming of this approach is that it does not allow quantifiers inside goals sent to SMT solvers, although it does not prevent one from feeding these solvers universally quantified lemmas. To increase the expressivity of SMTCoq with respect to quantifiers, one will need to switch to propositions, and handle classical logic either by axioms or by restricting attention to decidable atoms of the considered combined theory.

The first use case of this correct-by-construction checker is to check the validity of a proof witness, or proof certificate coming from an external solver against some input problem (Figure 1b). In this use case, the trusted base is both Coq and the parser of the input problem. The parse is part of the trusted based because we need to make sure we are effectively verifying a proof of the problem we sent to the external solver. However, this parser is fairly straightforward.

The second use case is within a Coq tactic (Figure 1c). We can give a Coq goal to an external solver and get a proof certificate for it. If the checker can validate the certificate, the soundness of the checker allow us to establish a proof of the initial goal. This process is known as computational reflection as it uses a computation (here, the execution of the checker) inside a proof. In this use case, the trusted base consists only of Coq: if something else goes wrong (e.g., the checker cannot validate the certificate), the tactic will fail, but nothing unsound will be added to the system.

In both cases, a crucial aspect for modularity purposes is the possibility to preprocess proof certificates before sending them to the SMTCoq checker, without having to prove anything about this preprocessing stage. Again, if the preprocessor is buggy, the checker will fail to validate the proof certificate (by returning false), which means that while nothing is learned, nothing unsafe is added to Coq's context. This allows us to easily extend SMTCoq with new solvers: as long as the certificate coming from the new solver can be logically encoded into SMTCoq's certificate format, we can implement this encoding at the preprocessing stage. As a result, SMTCoq's current support for both ZChaff and veriT is provided through the implementation of a preprocessor for each solver. Both preprocessors convert to the same proof format, thus sharing the same checker.

Using a preprocessor is also beneficial for efficiency: proof certificates may be encoded more compactly before being sent to the SMTCoq checker, which may improve performance.

The Checker

We now provide more details on the checker of SMTCoq. As presented in Figure 2, it consists of a main checker obtained as the combination of several small checkers, each specialized in one aspect of proof SMTCoq checking in SMT (e.g., CNF conversion, propositional reasoning, reasoning in the theory of equality, linear arithmetic reasoning, and so on). The type certificate is actually the aggregation of specialized types, one for each small checker. The role of the main checker is thus to dispatch each piece of the certificate to its dedicated small checker, until the initial formula is proved.

A small checker is a Coq program that, given a (possibly empty) list of formulas and a certificate associated with it (which may be just a piece of the input certificate), computes a new formula:

small_checker : list formula → certificate_sc → formula
The soundness of the checker comes from the soundness of each small checker, stated as follows:

small_checker_sound : ∀ f 1 . . . f n c, f 1 ∧ . . . ∧ f n → small_checker [f 1 ;...;f n ] c
meaning that the small checker returns a formula which is implied (after translation into Coq's logic) by the conjunction of its premises. Note that the list of premises may be empty: in such a case, the small checker returns a tautology in Coq.

Here are some examples of small checkers.

• For propositional resolution chains, the checker takes as input a list of premises and returns a resolvent if it exists, or a trivially true clause otherwise. In this case, a certificate is not required as part of the small checker's input.

• For the theory of equality with uninterpreted functions (EUF), the checker takes as input a formula in this theory formulated as a certificate (corresponding to a theory lemma produced by the SMT solver), and returns the formula if it is able to check it, or a trivially true clause otherwise. In this case, no premises are given.

• For linear integer arithmetic (LIA), the checker works similarly to the EUF checker, but checks the formula using Micromega [START_REF] Besson | Fast Reflexive Arithmetic Tactics the Linear Case and Beyond[END_REF], an efficient decision procedure for this theory implemented in Coq.

The only thing that small checkers need to share is the type formula, and its interpretation into Coq Booleans. Each small checker may then reason independently, using separate pieces of the certificate. Again, this is crucial for modularity: to extend SMTCoq with a new theory, one only has to extend the type formula with the signature of this theory and, independently of the already existing checkers, implement a small checker for this theory and prove its soundness.

Notice that "small checker" can be understood in a very general sense: any function that, given a list of first-order formulas, returns an implied first-order formula, can be plugged into SMTCoq as a small checker. In principle, such a checker could even be as complex as an SMT solver, as long as it can be proved correct in Coq.

3 Work in Progress: Extensions to CVC4 and Bit Vector Arithmetic

Support for CVC4

CVC4 is a proof-producing SMT solver, whose proof format is based on the Logical Framework with Side Conditions (LFSC) [START_REF] Stump | SMT proof checking using a logical framework[END_REF]. LFSC extends the Edinburgh Logical Framework (LF) [START_REF] Harper | A Framework for Defining Logics[END_REF] by allowing types with computational side conditions, explicit computational checks defined as programs in a small but expressive functional first-order programming language. The language has built-in types for arbitrary precision integers and rationals, ML-style pattern matching over LFSC type constructors, recursion, a minimal support for exceptions, and a very restricted set of imperative features. One can define proof rules in LFSC as typing rules that may optionally include a side condition written in this language. When checking the application of such proof rules, an LFSC checker computes actual parameters for the side condition and executes its code; if the side condition fails, the LFSC checker rejects the rule application. The validity of an LFSC proof witness thus relies on the correctness of the side condition functions used in the proof. LFSC comes with a set of pre-defined side conditions for various theories, used by the CVC4 proof production mechanism.

The key differences between LFSC and the SMTCoq format are presented in Table 1.

LFSC SMTCoq Rules deduction + computation deduction + certificate Nested proofs supported not supported Table 1: Main differences between the LFSC and SMTCoq certificate formats

The major difference lies in the presentation of the deduction rules. In SMTCoq, the small checkers deduce a new formula from already known formulas, possibly with the help of a piece of certificate that depends on the theory. The LFSC format is more uniform, thanks to the side conditions described above.

To support LFSC, and so CVC4, we are in the process of implementing (in OCaml) an untrusted preprocessor that transforms LFSC proofs into SMTCoq proofs. To this end, for some theories, we need to replay parts of the side conditions, in order to produce the corresponding SMTCoq premises, conclusion and piece of certificate that will be passed to the small checkers. This encoding, however, is relatively straightforward:

• for propositional reasoning, LFSC side conditions use the same logical content as SMTCoq rules;

• CNF conversion and EUF proofs are nested in LFSC, so they require some processing for the moment;

• for linear integer arithmetic, since SMTCoq relies on an existing decision procedure in Coq, it only needs to know what theory lemma is being proved, and can ignore the actual proof steps in the LFSC certificate.

One difficulty in translating LFSC proofs to the SMTCoq format comes from to the possibility in LFSC of using natural-deduction-style proofs, where one can nest one proof inside another. For instance, it is possible to have lemmas inside an LFSC proof whose witnesses are themselves LFSC proofs. The architecture of the main and small checkers of SMTCoq does not currently allow this sort of nesting: every clause produced by the small checkers needs to be a direct consequence of input clauses or clauses that were previously produced. To encode an LFSC proof into SMTCoq, our preprocessor thus linearizes nested proofs. The LFSC proofs generated by CVC4 are constructed in such a way that this does not cause a blow-up in practice; however, to support LFSC in general, we plan to extend SMTCoq certificates with nested proofs. Again, this extension should be made easier by the modularity inside the checker. It should impact only the main checker, and not the various small checkers already in SMTCoq.

Support for Bit Vector Arithmetic

CVC4 has been recently extended to produce LFSC proofs for the quantifier-free fragment of the SMT theory of bit vectors [START_REF] Hadarean | Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors[END_REF]. To check proof certificates in this theory, SMTCoq needs be extended with it. As explained in Section 2.2, to do that one needs to:

1. extend the Coq representation of formulas with the signature of the bit vector theory and the interpretation function into Coq terms;

2. implement (new) small checkers and their corresponding certificates for this theory, and prove their correctness.

Step 1 is a simple extension on the SMTCoq side. The major difficulty is that Coq itself has limited support for bit vectors. Its bit vector library provides only the implementation of bitwise operations (and not arithmetic operations), and no proofs. We are thus currently implementing a more complete library for this theory. Step 2 involves implementing and adding new certified Coq programs (the small checkers). As mentioned, however, because of SMTCoq's design, none of the previous small checkers and their proofs of correctness need to be changed as a result of this addition.

LFSC proofs for bit vectors produce by CVC4 mainly involve the following two kinds of deduction steps:

• bit-blasting steps that reduce the input bit vector formula to an equisatisfiable propositional formula;

• standard propositional reasoning steps (based on resolution).

The propositional steps can be handled directly by previous small checkers. For the bit-blasting steps, we implemented new small checkers that relate terms of the bit vector theory with lists of Boolean formulas representing their bits; we are currently working on producing proofs of correctness in Coq for these small checkers. LFSC proofs generated by CVC4 involve a third kind of step: formula simplifications based on the equivalence of two bit-vector terms or atomic formulas (for instance, by normalizing inequalities). Currently, these simplification steps are not provided a detailed LFSC subproof by CVC4, although there are plans to do so in the near future. In the current SMTCoq implementation then, we assume those steps, as in the LFSC proof coming from CVC4, or let the user prove them, in the case of tactics. Since those steps correspond to applications of CVC4-defined rewriting and simplification rules, we plan for now to prove the correctness of these rules once and for all at the Coq level, and to pre-process simplification steps into applications of these rules.

Related Work

In addition to related work already discussed throughout the paper, we now briefly mention a few more notable projects. Heule et al. implemented an efficient checker for state-of-the-art SAT techniques, verified in ACL2 [START_REF] Heule | Verifying Refutations with Extended Resolution[END_REF][START_REF] Wetzler | Mechanical Verification of SAT Refutations with Extended Resolution[END_REF]. It is mainly based on a generalization of extended resolution [START_REF] Tseitin | On the Complexity of Proofs in Propositional Logics[END_REF][START_REF] Kullmann | On a Generalization of Extended Resolution[END_REF] and on reverse unit propagation [START_REF] Van Gelder | Producing and verifying extremely large propositional refutations -Have your cake and eat it too[END_REF]. SMTCoq currently handles only standard extended resolution for its propositional part.

Efficient proof reconstruction for SAT and SMT solvers has been implemented in proof assistants based on higher-order logic [START_REF] Weber | SAT-based Finite Model Generation for Higher-Order Logic[END_REF][START_REF] Böhme | Fast LCF-Style Proof Reconstruction for Z3[END_REF]. Some of these reconstructions also handle the theory of bit vectors [START_REF] Böhme | Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL[END_REF]. This approach is based on translating SAT/SMT certificates to applications of the inference rules of the kernels of these proof assistants. In contrast, our approach in Coq is based on computational reflection: the certificate is directly processed by the reduction mechanism of Coq's kernel.

Based on an efficient encoding of a large subset of HOL goals into first-order logic, the Sledgehammer tactic [START_REF] Lawrence | Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers[END_REF] allows HOL-based proof assistants to efficiently and reliably help manual proving. Proofs are replayed using either the proof reconstruction mechanism described above or a built-in first-order prover. We hope that SMTCoq can help in adding such techniques into Coq and other Type Theorybased proof assistants, by providing a proof replay mechanism based on certificates.

Conclusion and Future Work

SMTCoq has been designed to be modular in such a way that facilities its extension with new solvers and new theories. In particular, such extensions should not require any changes in existing checkers or in their proofs of soundness. Thus, while it may require some effort to certify new small checkers or to translate new proof formats into the SMTCoq format, such extensions require only local changes. Our current extensions to CVC4 and bit vectors arithmetic validate this goal: indeed, the work so far consisted mostly in implementing an untrusted preprocessor for certificates and adding new, independent checkers. One limiting aspect of SMTCoq is the lack of support for nested proofs, which we plan to add. Thanks to the modularity of the checker, we believe this feature too can be added locally.

In the future we plan to continue extending the expressivity of SMTCoq, and in particular to offer support for the SMT theory of arrays (for which CVC4 is also proof-producing). We believe we can match, and perhaps even improve upon existing work in terms of efficiency.

The current major limitation of SMTCoq resides in its set of tactics: presently, it can only handle goals that are directly provable by SMT solvers, without much encoding of Coq logic into first-order logic. Our longer term plan is to combine ongoing work on hammering [START_REF] Christian Blanchette | Hammering towards QED[END_REF] for proof assistants based on Type Theory (such as Coq) with the certificate checking capabilities offered by SMTCoq.

Figure 1 :

 1 Figure 1: SMTCoq's main checker and its uses

Figure 2 :

 2 Figure 2: Internals of the Coq checker

SMTCoq is distributed as free software at https://github.com/smtcoq/smtcoq.

Acknowledgments. We wish to thank the anonymous reviewers for their helpful and constructive feedback. This work was supported in part by the Air Force Research Laboratory (AFRL) and the Defense

SMTCoq

Advanced Research Projects Agency (DARPA) under contracts FA8750-13-2-0241 and FA8750-15-C-0113. Any opinions, findings, and conclusions or recommendations expressed above are those of the authors and do not necessarily reflect the views of AFRL or DARPA.


Javier Nuño

Christophe Finot

Julien Fatome

Linear Sampling and Magnification Technique Based on Phase Modulators and Dispersive Elements: the Temporal Lenticular Lens

Keywords: All-optical signal processing, fiber devices, linear sampling, phase modulation, dispersion

In this work, we exploit the space/time duality in optics to implement a temporal lenticular lens allowing to simultaneously sample and magnify an arbitrary-shaped optical signal. More specifically, by applying a sinusoidal phase-modulation, the signal under test is propagated through a discrete dispersive element that samples and magnifies its initial waveform. Thanks to this temporal lenticular lens, optical sampling associated to a magnification factor of 3.6 is experimentally demonstrated at a repetition rate of 10 GHz.

Introduction

In modern photonic systems, the sampling process has widespread applications in the fields of optical communications, metrology, clocking, sensing, spectral comb or arbitrary waveform generation. In this context, nonlinear effects have been demonstrated as potential key technologies to develop all-optical sampling devices [START_REF] Duguay | An ultrafast ligth gate[END_REF]- [START_REF] Xu | Photonic analog-to-digital converter using soliton self-frequency shift and interleaving spectral filters[END_REF]. Most of these methods are based on the nonlinear interaction among a train of ultrashort high-power pulses and the original signal, thus requiring an external mode locked picosecond pulse source. The basic physical phenomena involved in these interactions include four-wave mixing [START_REF] Oda | All-optical quantization scheme based on fiber nonlinearity[END_REF], cross-phase modulation (XPM) [START_REF] Li | 0.5-Tb/s eye-diagram measurement by optical sampling using XPM-induced wavelength shifting in highly nonlinear fiber[END_REF], nonlinear polarization rotation [START_REF] Zhang | All-optical sampling exploiting nonlinear polarization rotation in a single semiconductor optical amplifier[END_REF] or Raman soliton self-frequency shift [START_REF] Xu | Photonic analog-to-digital converter using soliton self-frequency shift and interleaving spectral filters[END_REF].

More recently, an alternative nonlinear approach has been experimentally demonstrated at a sampling rate of 40 GHz, whilst providing a simultaneous 8-dB magnification factor of the waveform [START_REF] Nuño | All-optical sampling and magnification based on XPM-induced focusing[END_REF]. Basically, during its co-propagation in a km-long fiber with a high-power sinusoidal pump beam, the waveform under test experiences a strong temporal phase modulation due to the XPM coupling. Subsequently, the signal undergoes a simultaneous temporal compression due to the normal dispersion regime of the fiber, leading to a periodic and localized nonlinear focusing effect [START_REF] Nuño | 40 GHz pulse source based on cross-phase modulation-induced focusing in normally dispersive optical fibers[END_REF]. In this new contribution, we propose a linear implementation of this process that does not require any external optical sampling beam. More precisely, here an electro-optic modulator is used to imprint the initial temporal phase modulation, while a programmable and compact spectral phase shaper enables an optimum sampling process through the formation of periodic pulses proportional to the initial waveform. Based on the analogy that can be drawn between usual spatial optics and ultrafast optics [START_REF] Kolner | Space-time duality and the theory of temporal imaging[END_REF]- [START_REF] Van Howe | Ultrafast Optical Signal Processing Based Upon Space-Time Dualities[END_REF], such approach mimics in the temporal domain the behavior of a periodic lenticular lens that focuses different parts of an illuminating plane wave at equally spaced positions.

Our manuscript is organized as follows. In the second section, we describe the principle of our method and in particular, we highlight the analogy with the lenticular lens. Subsequently, we also present some design guidelines related to the magnification factor and optimum dispersion. In sections 3, we then describe the experimental linear setup we implemented. The experimental results are presented in section 4 and are compared with numerical simulations, demonstrating an excellent agreement. Finally, in section 5, we summarize our work and trace out some conclusions and outlooks.

Principle of operation and design rules

Frequency chirp compensation of a parabolic time-dependent phase modulated signal passing through a dispersive medium imposing a quadratic spectral phase is a widely spread technique to produce ultrashort structures [START_REF] Giordmaine | Compression of optical pulses[END_REF]. More generally, this focusing process can be viewed as the temporal analogue of an optical lens by using the space-time duality [START_REF] Kolner | Temporal imaging with a time lens[END_REF]- [START_REF] Godil | Picosecond time-lenses[END_REF].

To imprint such an initial modulation within an incoming signal, taking advantage of the Kerr nonlinearity in optical fibers has been proved to be an attractive and efficient approach, for instance through self-or cross-phase modulation processes [START_REF] Grischkowsky | Optical pulse compression based on enhanced frequency chirping[END_REF]- [START_REF] Wang | Degenerate cross-phase modulation for pulse compression and amplification of ultrashort laser pulses[END_REF]. In a recent work, we have suggested and experimentally demonstrated an all-fibered sampling technique based on the XPM induced by a sinusoidal pump beam on the signal under test (SUT) combined to a simultaneous adiabatic compensation through normal chromatic dispersion [START_REF] Nuño | All-optical sampling and magnification based on XPM-induced focusing[END_REF]. In this configuration, the SUT experiences periodic local compression, leading to an efficient sampling and magnification of its waveform.

An alternative approach to imprint such initial temporal phase modulation is to benefit from electro-optic devices [START_REF] Grischkowsky | Optical Pulse Compression[END_REF]. Based on standard off-the-shelf telecom platform, this linear method has been proved more stable, less complex as well as more power efficient than nonlinear techniques. However, lower phase modulation amplitude can be achieved, so cascading several phase modulators is often required to achieve large frequency chirps [START_REF] Yamamoto | High-reflectivity-resolution coherent optical frequency domain reflectometry using optical frequency comb source and tunable delay line[END_REF].

Moreover, due to experimental constraints, synthetizing a perfect temporal quadratic phase modulation is quite difficult to achieve so most of the time, the initial modulation is replaced by a sinusoidal waveform that is close to a parabola at its extrema. In this case, when driven by RF sinusoidal signals, it is well known that the phase modulation of an initial continuous wave (CW) leads to the generation of high-repetition rate pulse trains after its propagation in a dispersive element [START_REF] Komukai | Optical pulse generator using phase modulator and linearly chirped fiber Bragg gratings[END_REF]- [START_REF] Kobayashi | Optical pulse compression using high-frequency electrooptic phase modulation[END_REF]. By exploiting the space-time duality, as depicted in Fig. 1(a), such method of periodic temporal focusing presents some analogy with lenticular lenses in geometric optics where lenses are periodically reproduced and for which an incoming plane wave is focused at different equally spaced points. (3). In the inset, the maximum magnifying factor for each phase is plotted. The yellow circle represents the values in our experiments (θ =0.55π and D ≈145 ps•nm -1 in the fiber). In both cases, the frequency is equal to 10 GHz.

In this novel contribution, we exploit a similar physical principle as the basis of our linear sampler. As depicted in Fig. 1(b), the modulation of the temporal phase produces a frequency chirp and in a second stage, a dispersive element that can be a linear optical fiber segment, a fiber Bragg grating [START_REF] Komukai | Optical pulse generator using phase modulator and linearly chirped fiber Bragg gratings[END_REF], a pair of diffraction gratings [START_REF] Kobayashi | Optical pulse compression using high-frequency electrooptic phase modulation[END_REF] or a programmable spectral filter [START_REF] Roelens | Dispersion trimming in a reconfigurable wavelength selective switch[END_REF] imprints a quadratic spectral phase that temporally redistribute and concentrate the energy of the SUT in the central points. Consequently, the resulting signal is sampled at the frequency of the modulation and the peak power at these points is proportional to the initial waveform which is subsequently magnified in a noiseless process [START_REF] Maram | Noiseless intensity amplification of repetitive signals by coherent addition using the temporal Talbot effect[END_REF]. Note that in contrast to our preceding work published in ref. [START_REF] Nuño | All-optical sampling and magnification based on XPM-induced focusing[END_REF] and for which the regime of chromatic dispersion had to be normal, here it can be chosen either anomalous or normal.

The design of our sampling device is rather simple as the final waveform is fully determined by only three parameters: the amplitude (θ) and frequency (f m ), associated with the temporal sinusoidal phase modulation and the accumulated dispersion (D) linked to the quadratic spectral phase of the second stage. Note that to be fully efficient, the period of the modulation has to be much shorter than the temporal width of the SUT. The sampled waveform I out (t) can indeed be derived from the SUT I in (t) (which is here assumed for simplicity to be Fourier transformed) by the following formula :

(1)

    2 2 2 1 in 1 ( ) ( ) exp( cos(2 ) exp 2 2 2 out m I t F F I t i f t i D f c                        
with c being the speed of light,  the central wavelength of the SUT, t and f being the temporal and frequency coordinates respectively. F and F -1 stand for the direct and inverse Fourier transform respectively. The magnifying factor G (defined as the power obtained at the sampling time, i.e. the peak-power of the resulting ultrashort pulse, divided by the power of the SUT at the same instant before sampling) can be inferred based on the following formula derived in the case of a quasi-continuous wave:

(2)

    2 2 2 1 1 ( , , ) max exp( cos(2 ) exp 2 2 2 m m G D f F F i f t i D f c                                   
Results of Eq. ( 2) for f m fixed to 10 GHz are plotted in Fig. 1(c) and show that for each amplitude, the optimum performances (i.e. maximum peak power) are reached for a welldefined dispersion value as predicted by Kokumai in ref. [START_REF] Komukai | Optical pulse generator using phase modulator and linearly chirped fiber Bragg gratings[END_REF] with the approximate formula:

(

2 1 1 30. 45 12.56

opt m c D f      
Therefore when modulation amplitude is increased, the best performance is obtained for a lower total dispersion. At the same time, as can be seen in the inset of Fig. 1(c), the higher the modulation amplitude is, the higher the magnifying factor is.

Experimental setup

For validating this proposed concept at telecommunication wavelengths, we have implemented the experimental setup depicted in Fig. 2 and made exclusively of commercially available components. In order to generate the nanosecond SUT, an external cavity laser emitting at 1550 nm is firstly intensity modulated by means of an intensity modulator (IM) that is driven by the electrically filtered output of a pulse pattern generator (PPG) delivering an arbitrary shaped ns signal at a repetition rate of 9.77 MHz. Although the performance of this system is independent on the signal power, this wave is amplified up to 10 dBm to avoid a weak signal in the reception stage. Subsequently, the sinusoidal phase is induced in the signal thanks to a phase modulator (PM) driven by a 10 GHz electrical clock that also synchronizes the PPG and the high bandwidth electrical sampling oscilloscope. Compared to our previous work of ref. [START_REF] Nuño | All-optical sampling and magnification based on XPM-induced focusing[END_REF], the use of the PM offers significant advantages in terms of stability and controllability and does not require to involve any high power pulsed wave that has to be polarization multiplexed. The parabolic spectral phase is imprinted on the signal thanks to a liquid-crystal on silicium programmable filter [START_REF] Roelens | Dispersion trimming in a reconfigurable wavelength selective switch[END_REF] (Finisar Waveshaper device). As the performance of this filter is limited to a total dispersion lower than 80 ps.nm -1 , we have introduced a 10-km span of single-mode fiber whose dispersion parameter is -14.5 ps/nm/km. Consequently, the compensating module achieves a total dispersion (|D|) close to 145 ps.nm -1 .

Finally, the signal is analyzed in the time domain thanks to an electrical sampling oscilloscope (ESO) with a 70-GHz bandwidth of detection as well as in the optical and electrical spectral domains by means of a high-resolution optical spectrum analyzer (OSA) and a RF spectrum analyzer (RFSA), respectively.

Experimental results

To fully assess that the present technique enables to sample an arbitrary shaped optical signal without any distortion, we first compare in Fig. 3(a) the normalized input and output intensity profiles obtained for an amplitude of phase modulation of θ = 0.55 π and |D| equals to 125 ps.nm -1 (which was the optimum experimental value for this set of parameters). We can observe that the output waveform (in orange solid line) corresponds to a 10-GHz sampled replica of the initial SUT (blue dotted line) and more specifically, that the details of the signal are accurately reproduced without any distortion independently of the SUT level and complexity. Figure 3(b) displays a close view on only seven temporal periods of the phase modulation and confirms the above assumptions. We observe that the full width at half maximum (FWHM) duration of the compressed structures is less than 20 ps. These pulses lie on a residual background that we attribute to the sinusoidal modulation that we employ instead of a perfect parabolic modulation of the temporal phase required for a perfect time-lens. The numerical estimations of Eq. ( 1) have also been included in the figure in green dashed-line and provide an excellent agreement with our experimental results, thus validating our design rules.

The magnification process can be observed in Fig. 4(a). The intensity profile of the output wave (in orange) corresponds to a temporal intensity comb whose magnitude is exactly proportional to the input signal with an amplitude 3.6 times higher than the one observed when PM is turned off (blue line). In order to check the crucial role played by the quadratic spectral phase, we have recorded the magnifying factor for different values of dispersion. Combining measurements of the spectral shaper alone and the association of the dispersive fiber span with the programmable filter has enabled us to explore the dispersion values |D| ranging from 0 up to 160 ps/km/nm. Results are summarized in Fig. 4(b). Following the trends observed in Fig. 1(c), the magnification factor is increasing with the total dispersion until the optimum focusing point is reached. In our experiment a maximum magnifying factor of 3.6 is achieved, which is only 11% lower than the numerical estimations of Eq. 2. Note that the experimental results are in quantitative agreement with predictions of Eq. ( 2) for a modulation amplitude θ of 0.55 π (yellow line). Finally, the output signal is analyzed in the optical and the RF spectral domains. In the optical domain, the sampling process is characterized by the generation of replicas of the initial waveform regularly spaced by the modulation frequency (10 GHz) as can be seen in Fig. 5(a).

The levels of these replica are in excellent agreement with our assumption of a sinusoidal phase modulation having a 0.55  rad amplitude and calculated according to Eq. (1) (orange crosses). The optical signal to noise ratio is also excellent, as expected from this noiseless magnification process. Similarly, the initial SUT is reproduced in every 10-GHz harmonics in the RF spectrum with an excellent signal to noise ratio (see Fig.

Conclusions

In conclusion, we have suggested and experimentally demonstrated a novel approach to simultaneously sample and magnify the temporal intensity profile of an arbitrary shaped optical signal. Owing to the space/time duality, this technique exploits the temporal analogue of lenticular lenses for which an incoming plane wave is focused at different equally spaced points.

Inspired by a previous nonlinear sampler where Kerr nonlinearity and dispersion act simultaneously and adiabatically in a km-long fiber [START_REF] Nuño | All-optical sampling and magnification based on XPM-induced focusing[END_REF], here we proposed a new linear implementation where tailoring of the temporal and spectral phase profiles are achieved independently by use of compact devices. Moreover, our new implementation has relaxed the need of an external optical high power sampling beam while the use of a programmable spectral shaper offers flexibility to find the optimum operating parameters according to the frequency and amplitude of the temporal phase modulation.

We have experimentally validated our approach by sampling a nanosecond arbitrary shaped signal at a frequency of 10 GHz. A magnification factor of 3.6 has been achieved in this proofof-principle experiment. Higher magnifying factor could be reached if the amplitude of the phase modulation is increased up to the levels of a dozen of  rad that are already available in the literature. Cascaded phase modulators can also be a solution to improve the results [START_REF] Godil | Picosecond time-lenses[END_REF], [START_REF] Yamamoto | High-reflectivity-resolution coherent optical frequency domain reflectometry using optical frequency comb source and tunable delay line[END_REF]. The aberrations caused by the sinusoidal modulation could be reduced with the current progress of microwave photonic. Finally, let us note that an alternative to the present setup where the second stage induces a parabolic spectral phase could be to use a sharp filter with a central wavelength shifted with respect to incoming signal [START_REF] Chapman | All-fiber integrated 10 GHz repetition rate femtosecond laser source based on Raman compression of pulses generated through spectral masking of a phase-modulated diode[END_REF]. The advantage would be to generate shorter structures, but at the cost of a severe dissipative process that prevents any magnification.

Fig. 1 .

 1 Fig. 1. (a) Lenticular lens illuminated by a plane wave. (b) Principle of the proposed temporal approach. (c) Magnifying factor as a function of both the amplitude θ of the phase modulation and the amount of chromatic dispersion. The dotted line represents the maximum magnifying factor according to the approximate prediction given by Eq.

Fig. 2 .

 2 Fig. 2. Experimental setup. IM: intensity modulator, PM: phase modulator, PPG: pulse pattern generator, EDFA: Erbium doped fiber amplifier, ESO: electrical sampling oscilloscope, OSA: optical spectrum analyzer and RFSA: RF spectrum analyzer.

Fig. 3 .

 3 Fig. 3. (a) Normalized intensity profiles of the input (blue dotted line) and output (red line) signals for D = -125 ps.nm -1 in the temporal domain. The green dashed line represents the numerical estimation of Eq. (1). The phase amplitude (Vpp/2) is 0.55 π and f m = 10 GHz. (b)Close view of (a). Results are normalized to 1 for their maximum value.

Fig. 4 .

 4 Fig. 4. (a) Intensity profiles of the input (blue dotted line) and output (orange line) signals for D = -125 ps.nm -1 in the temporal domain. (b) Experimental magnifying factor as function of the total dispersion of the module obtained with the spectral shaper alone (black circles) and with the combination of dispersive fiber and spectral shaper (blue crosses). Experimental results are compared with the numerical estimation based on Eq. 2 (yellow line).

  5(b)).

Fig. 5 .

 5 Fig. 5. Spectra of the signal after sampling in the optical domain (a) and in the electrical domain (b) In Fig. 4(a), the maxima of the numerical estimation based on the assumption of a sinusoidal modulation with an amplitude of 0.55  rad are indicated with orange crosses. The inset of Fig. 4(b) represents a close view of the RF spectrum and the spacing between the spectral lines corresponds to the repetition rate of the SUT delivered by the PPG (9.77 MHz).

Acknowledgments

We acknowledge fruitful discussions with Hervé Rigneault regarding the space-time analogies. This research is funded by the European Research Council under Grant Agreement 306633, ERC PETAL (www.facebook.com/petal.inside). The authors would like to acknowledge support by the Région Bourgogne (Pari Photcom) and the Agence Nationale de la Recherche (Labex Action ANR-11-LABX-0001-01).