The Locality of Memory Checking

被引:3
|
作者
Wang, Weijie [1 ]
Lu, Yujie [1 ]
Papamanthou, Charalampos [1 ]
Zhang, Fan [1 ]
机构
[1] Yale Univ, New Haven, CT 06520 USA
基金
美国国家科学基金会;
关键词
Memory checking; foundations of cryptography;
D O I
10.1145/3576915.3623195
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Motivated by the extended deployment of authenticated data structures (e.g., Merkle Patricia Tries) for verifying massive amounts of data in blockchain systems, we begin a systematic study of the I/O efficiency of such systems. We first explore the fundamental limitations of memory checking, a previously-proposed abstraction for verifiable storage, in terms of its locality-a complexity measure that we introduce for the first time and is defined as the number of non-contiguous memory regions a checker must query to verifiably answer a read or a write query. Our central result is an Omega( log n/log log n) lower bound for the locality of any memory checker. Then we turn our attention to (dense and sparse) Merkle trees, one of the most celebrated memory checkers, and provide stronger lower bounds for their locality. For example, we show that any dense Merkle tree layout will have average locality at least 1/3 log n. Furthermore, if we allow node duplication, we show that if any write operation has at most polylog complexity, then the read locality cannot be less than log n/log log n. Our lower bounds help us construct two new locality-optimized authenticated data structures (DupTree and PrefixTree) which we implement and evaluate on random operations and real workloads, and which are shown to outperform traditional Merkle trees, especially as the number of leaves increases.
引用
收藏
页码:1820 / 1834
页数:15
相关论文
共 50 条
  • [41] MemSAT: Checking Axiomatic Specifications of Memory Models
    Torlak, Emina
    Vaziri, Mandana
    Dolby, Julian
    ACM SIGPLAN NOTICES, 2010, 45 (06) : 341 - 350
  • [42] Scalable shared memory LTL model checking
    Barnat J.
    Brim L.
    Ročkai P.
    International Journal on Software Tools for Technology Transfer, 2010, 12 (02) : 139 - 153
  • [43] Joint forces for memory safety checking revisited
    Chalupa, Marek
    Strejcek, Jan
    Vitovska, Martina
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2020, 22 (02) : 115 - 133
  • [44] Flash memory efficient LTL model checking
    Edelkamp, S.
    Sulewski, D.
    Barnat, J.
    Brim, L.
    Simecek, P.
    SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (02) : 136 - 157
  • [45] Memory bias, confidence and responsibility in compulsive checking
    Radomsky, AS
    Rachman, S
    Hammond, D
    BEHAVIOUR RESEARCH AND THERAPY, 2001, 39 (07) : 813 - 822
  • [46] Can Flash Memory Help in Model Checking?
    Barnat, Jiri
    Brim, Lubos
    Edelkamp, Stefan
    Sulewski, Damian
    Simecek, Pavel
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2009, 5596 : 150 - +
  • [47] MemSAT: Checking Axiomatic Specifications of Memory Models
    Torlak, Emina
    Vaziri, Mandana
    Dolby, Julian
    PLDI '10: PROCEEDINGS OF THE 2010 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2010, : 341 - 350
  • [48] Distributed-memory model checking with SPIN
    Lerda, F
    Sisto, R
    THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING, 1999, 1680 : 22 - 39
  • [49] Joint forces for memory safety checking revisited
    Marek Chalupa
    Jan Strejček
    Martina Vitovská
    International Journal on Software Tools for Technology Transfer, 2020, 22 : 115 - 133
  • [50] HMC: Model Checking for Hardware Memory Models
    Kokologiannakis, Michalis
    Vafeiadis, Viktor
    TWENTY-FIFTH INTERNATIONAL CONFERENCE ON ARCHITECTURAL SUPPORT FOR PROGRAMMING LANGUAGES AND OPERATING SYSTEMS (ASPLOS XXV), 2020, : 1157 - 1171