Skip to main content

2017 | OriginalPaper | Buchkapitel

PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing

verfasst von : Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiří Srba

Erschienen in: Theoretical Aspects of Computing – ICTAC 2017

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Sets and their efficient implementation are fundamental in all of computer science, including model checking, where sets are used as the basic data structure for storing (encodings of) states during a state-space exploration. In the quest for fast and memory efficient methods for manipulating large sets, we present a novel data structure called PTrie for storing sets of binary strings of arbitrary length. The PTrie data structure distinguishes itself by compressing the stored elements while sharing the desirable key characteristics with conventional hash-based implementations, namely fast insertion and lookup operations. We provide the theoretical foundation of PTries, prove the correctness of their operations and conduct empirical studies analysing the performance of PTries for dealing with randomly generated binary strings as well as for state-space exploration of a large collection of Petri net models from the 2016 edition of the Model Checking Contest (MCC’16). We experimentally document that with a modest overhead in running time, a truly significant space-reduction can be achieved. Lastly, we provide an efficient implementation of the PTrie data structure under the GPL version 3 license, so that the technology is made available for memory-intensive applications such as model-checking tools.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
Both these extension come with a smaller overhead in run-time and memory. Also, currently neither of these extensions support Delete.
 
Literatur
1.
Zurück zum Zitat Askitis, N., Sinha, R.: HAT-trie: a cache-conscious trie-based data structure for strings. In: Proceedings of the Thirtieth Australasian Conference on Computer Science, vol. 62, pp. 97–105. Australian Computer Society Inc. (2007) Askitis, N., Sinha, R.: HAT-trie: a cache-conscious trie-based data structure for strings. In: Proceedings of the Thirtieth Australasian Conference on Computer Science, vol. 62, pp. 97–105. Australian Computer Society Inc. (2007)
2.
Zurück zum Zitat Bagwell, P.: Ideal hash trees. Es Grands Champs, vol. 1195 (2001) Bagwell, P.: Ideal hash trees. Es Grands Champs, vol. 1195 (2001)
3.
Zurück zum Zitat Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C–35(8), 677–691 (1986)CrossRefMATH Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C–35(8), 677–691 (1986)CrossRefMATH
4.
Zurück zum Zitat Byg, J., Jørgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc petri nets. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 84–89. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_7 CrossRef Byg, J., Jørgensen, K.Y., Srba, J.: TAPAAL: editor, simulator and verifier of timed-arc petri nets. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 84–89. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-04761-9_​7 CrossRef
8.
Zurück zum Zitat David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_36 CrossRef David, A., Jacobsen, L., Jacobsen, M., Jørgensen, K.Y., Møller, M.H., Srba, J.: TAPAAL 2.0: integrated development environment for timed-arc petri nets. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 492–497. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28756-5_​36 CrossRef
9.
Zurück zum Zitat Evangelista, S., Pradat-Peyre, J.-F.: Memory efficient state space storage in explicit software model checking. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 43–57. Springer, Heidelberg (2005). doi:10.1007/11537328_7 CrossRef Evangelista, S., Pradat-Peyre, J.-F.: Memory efficient state space storage in explicit software model checking. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 43–57. Springer, Heidelberg (2005). doi:10.​1007/​11537328_​7 CrossRef
10.
Zurück zum Zitat Evans, J.: A scalable concurrent malloc (3) implementation for FreeBSD. In: Proceedings of the BSDCan Conference Ottawa (2006) Evans, J.: A scalable concurrent malloc (3) implementation for FreeBSD. In: Proceedings of the BSDCan Conference Ottawa (2006)
11.
12.
Zurück zum Zitat Gwehenberger, G.: Anwendung einer binären verweiskettenmethode beim aufbau von listen/use of a binary tree structure for processing files. IT Inf. Technol. 10(1–6), 223–226 (1968)MATH Gwehenberger, G.: Anwendung einer binären verweiskettenmethode beim aufbau von listen/use of a binary tree structure for processing files. IT Inf. Technol. 10(1–6), 223–226 (1968)MATH
13.
Zurück zum Zitat Heinz, S., Zobel, J., Williams, H.E.: Burst tries: a fast, efficient data structure for string keys. ACM Trans. Inf. Syst. 20, 192–223 (2002)CrossRef Heinz, S., Zobel, J., Williams, H.E.: Burst tries: a fast, efficient data structure for string keys. ACM Trans. Inf. Syst. 20, 192–223 (2002)CrossRef
14.
Zurück zum Zitat Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307–318. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53401-4_16 CrossRef Jensen, J.F., Nielsen, T., Oestergaard, L.K., Srba, J.: TAPAAL and reachability analysis of P/T nets. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 307–318. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-53401-4_​16 CrossRef
15.
Zurück zum Zitat Jensen, P.G., Larsen, K.G., Srba, J., Sørensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307–312. Springer, Cham (2014). doi:10.1007/978-3-319-06200-6_26 CrossRef Jensen, P.G., Larsen, K.G., Srba, J., Sørensen, M.G., Taankvist, J.H.: Memory efficient data structures for explicit verification of timed systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 307–312. Springer, Cham (2014). doi:10.​1007/​978-3-319-06200-6_​26 CrossRef
16.
Zurück zum Zitat Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trịnh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http://mcc.lip6.fr/2016/results.php Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trịnh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http://​mcc.​lip6.​fr/​2016/​results.​php
17.
Zurück zum Zitat Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22306-8_4 CrossRef Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22306-8_​4 CrossRef
18.
Zurück zum Zitat Morrison, D.R.: Patriciapractical algorithm to retrieve information coded in alphanumeric. J. ACM (JACM) 15(4), 514–534 (1968)CrossRef Morrison, D.R.: Patriciapractical algorithm to retrieve information coded in alphanumeric. J. ACM (JACM) 15(4), 514–534 (1968)CrossRef
19.
Zurück zum Zitat Prokopec, A., Bronson, N.G., Bagwell, P., Odersky, M.: Concurrent tries with efficient non-blocking snapshots. ACM SIGPLAN Not. 47(8), 151–160 (2012). ACMCrossRef Prokopec, A., Bronson, N.G., Bagwell, P., Odersky, M.: Concurrent tries with efficient non-blocking snapshots. ACM SIGPLAN Not. 47(8), 151–160 (2012). ACMCrossRef
21.
Zurück zum Zitat Ročkai, P., Štill, V., Barnat, J.: Techniques for memory-efficient model checking of C and C++ code. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 268–282. Springer, Cham (2015). doi:10.1007/978-3-319-22969-0_19 CrossRef Ročkai, P., Štill, V., Barnat, J.: Techniques for memory-efficient model checking of C and C++ code. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 268–282. Springer, Cham (2015). doi:10.​1007/​978-3-319-22969-0_​19 CrossRef
24.
Zurück zum Zitat Wolf, K.: Running LoLA 2.0 in a model checking competition. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 274–285. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53401-4_13 CrossRef Wolf, K.: Running LoLA 2.0 in a model checking competition. In: Koutny, M., Desel, J., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency XI. LNCS, vol. 9930, pp. 274–285. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-53401-4_​13 CrossRef
Metadaten
Titel
PTrie: Data Structure for Compressing and Storing Sets via Prefix Sharing
verfasst von
Peter Gjøl Jensen
Kim Guldstrand Larsen
Jiří Srba
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-67729-3_15