Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Model Checking and Artificial Intelligence

MoChArt 2010: Model Checking and Artificial Intelligence pp 12–31Cite as

External Memory Breadth-First Search with Delayed Duplicate Detection on the GPU

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6572))

Abstract

We accelerate breadth-first search by delegating complex operations to the graphics processing unit (GPU). The algorithm exploits external memory: if the state space becomes too large to be kept in main memory, it is maintained I/O-efficiently on disk.

As in many other approaches for external memory graph search, we apply delayed duplicate detection. The search proceeds in breadth-first layers with increasing minimum distance from the start state. For each layer stored on disk, we load chunks into the systems memory, which are forwarded to the memory on the graphics card. Here we test if outgoing transitions are enabled and generate all successors. Finally, we eliminate duplicates delayed by sorting on the GPU. Even facing the overhead of I/O access, noticeable overall speed-ups are obtained.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ajwani, D., Dementiev, R., Meyer, U.: A computational study of external-memory BFS algorithms. In: ACM-SIAM Symposium On Discrete Algorithms (SODA), pp. 601–610 (2006)

    Google Scholar 

  2. Barnat, J., Brim, L., Ročkai, P.: Scalable multi-core LTL model-checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 187–203. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Barnat, J., Brim, L., Češka, M.: DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science (PDMC) 14, 107–111 (2009)

    Article  Google Scholar 

  4. Barnat, J., Brim, L., Češka, M., Lamr, T.: CUDA accelerated LTL Model Checking. In: International Conference on Parallel and Distributed Systems (ICPADS 2009), pp. 34–41 (2009)

    Google Scholar 

  5. Barnat, J., Brim, L., Šimeček, P.: I/O efficient accepting cycle detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 281–293. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Barnat, J., Brim, L., Šimeček, P., Weber, M.: Revisiting resistance speeds up I/O-efficient LTL model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 48–62. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Batcher, K.E.: Sorting networks and their applications. AFIPS Spring Joint Computing Conference 32, 307–314 (1968)

    Google Scholar 

  8. Belazzougui, D., Botelho, F.C., Dietzfelbinger, M.: Hash, displace, and compress. In: Fiat, A., Sanders, P. (eds.) ESA 2009. LNCS, vol. 5757, pp. 682–693. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Bloom, D.: A birthday problem. American Mathematical Monthly 80, 1141–1142 (1973)

    Article  MathSciNet  Google Scholar 

  10. Botelho, F.C., Ziviani, N.: External perfect hashing for very large key sets. In: ACM Conference on Information and Knowledge Management (CIKM), pp. 653–662 (2007)

    Google Scholar 

  11. Brizzolari, F., Melatti, I., Tronci, E., Penna, G.D.: Disk based software verification via bounded model checking. In: Asia-Pacific Software Engineering Conference (APSEC), pp. 358–365 (2007)

    Google Scholar 

  12. Burks, A.W., Warren, D.W., Wright, J.B.: An analysis of a logical machine using parenthesis-free notation. Mathematical Tables and Other Aids to Computation 8(46), 53–57 (1954)

    Article  MathSciNet  MATH  Google Scholar 

  13. Cederman, D., Tsigas, P.: A practical quicksort algorithm for graphics processors. In: Halperin, D., Mehlhorn, K. (eds.) Esa 2008. LNCS, vol. 5193, pp. 246–258. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  14. Cooperman, G., Finkelstein, L.: New methods for using Cayley graphs in interconnection networks. Discrete Applied Mathematics 37/38, 95–118 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  15. Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 1–18. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Edelkamp, S., Jabbar, S., Schrödl, S.: External A*. In: Biundo, S., Frühwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol. 3238, pp. 226–240. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Edelkamp, S., Sanders, P., Šimeček, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 530–542. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: International Conference on Software Engineering and Formal Methods (SEFM), pp. 73–82 (2008)

    Google Scholar 

  19. Edelkamp, S., Sulewski, D.: Model checking via delayed duplicate detection on the GPU. Technical Report 821, Technische Universität Dortmund. Presented on the 22nd Workshop on Planning, Scheduling, and Design PUK 2008 (2008)

    Google Scholar 

  20. Edelkamp, S., Sulewski, D., Yücel, C.: Perfect hashing for domain-dependent planning on the gpu. In: International Conference on Automated Planning and Scheduling, ICAPS (2010) (to appear)

    Google Scholar 

  21. Gastin, P., Moro, P.: Minimal counterexample generation for SPIN. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 24–38. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Govindaraju, N.K., Gray, J., Kumar, R., Manocha, D.: GPUTeraSort: High performance graphics coprocessor sorting for large database management. In: International Conference on Management of Data (SIGMOD), pp. 325–336 (2006)

    Google Scholar 

  23. Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)

    Google Scholar 

  24. Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design 13(3), 287–305 (1998)

    Article  MathSciNet  Google Scholar 

  25. Jabbar, S.: External Memory Algorithms for State Space Exploration in Model Checking and Action Planning. PhD thesis, Technical University of Dortmund (2008)

    Google Scholar 

  26. Knuth, D.E.: The Art of Computer Programming. Addison-Wesley, Reading (1973)

    MATH  Google Scholar 

  27. Korf, R.: Delayed duplicate detection: extended abstract. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1539–1541 (2003)

    Google Scholar 

  28. Korf, R.: Best-first frontier search with delayed duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 650–657 (2004)

    Google Scholar 

  29. Korf, R., Felner, A.: Recent progress in heuristic search: A case study of the Four-Peg Towers of Hanoi problem. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 2334–2329 (2007)

    Google Scholar 

  30. Korf, R., Schultze, P.: Large-scale parallel breadth-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 1380–1385 (2005)

    Google Scholar 

  31. Korf, R.E.: Breadth-first frontier search with delayed duplicate detection. In: MOCHART, pp. 87–92 (2003)

    Google Scholar 

  32. Korf, R.E.: Minimizing disk I/O in two-bit-breath-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 317–324 (2008)

    Google Scholar 

  33. Korf, R.E., Schultze, T.: Large-scale parallel breadth-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 1380–1385 (2005)

    Google Scholar 

  34. Lamborn, P., Hansen, E.: Layered duplicate detection in external-memory model checking. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 160–175. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  35. Leischner, N., Osipov, V., Sanders, P.: GPU sample sort. CoRR, abs/0909.5649 (2009)

    Google Scholar 

  36. Mehlhorn, K., Meyer, U.: External-memory breadth-first search with sublinear I/O. In: Möhring, R.H., Raman, R. (eds.) ESA 2002. LNCS, vol. 2461, pp. 723–735. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  37. Munagala, K., Ranade, A.: I/O-complexity of graph algorithms. In: SODA, pp. 687–694 (1999)

    Google Scholar 

  38. Nguyen, V.Y., Ruys, T.C.: Incremental hashing for spin. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 232–249. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  39. Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  40. Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT) 5(2-3), 185–204 (2004)

    Article  Google Scholar 

  41. Stern, U., Dill, D.L.: Combining state space caching and hash compaction. In: Methoden des Entwurfs und der Verifikation digitaler Systeme. GI/ITG/GME Workshop, vol. 4, pp. 81–90. Shaker Verlag, Aachen (1996)

    Google Scholar 

  42. Verstoep, K., Bal, H., Barnat, J., Brim, L.: Efficient Large-Scale Model Checking. In: International Symposium on Parallel and Distributed Processing, IPDPS (2009)

    Google Scholar 

  43. Vitter, J.S., Shriver, E.A.M.: Algorithms for parallel memory; I: two-level memories, II: hierarchical multilevel memories. Algorithmica 12(2/3), 110–169 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  44. Zhou, R., Hansen, E.A.: Structured duplicate detection in external-memory graph search. In: National Conference on Artificial Intelligence (AAAI), pp. 683–689 (2004)

    Google Scholar 

  45. Zhou, R., Hansen, E.A.: Parallel structured duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 1217–1222 (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TZI, Universität Bremen, Germany

    Stefan Edelkamp & Damian Sulewski

Authors
  1. Stefan Edelkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Damian Sulewski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and Engineering, University of New South Wales, 2052, Sydney, Australia

    Ron van der Meyden

  2. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, 79110, Freiburg, Germany

    Jan-Georg Smaus

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Edelkamp, S., Sulewski, D. (2011). External Memory Breadth-First Search with Delayed Duplicate Detection on the GPU. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-20674-0_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-20673-3

  • Online ISBN: 978-3-642-20674-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation