Cartesian partial-order reduction

被引:0
|
作者
Gueta, Guy [1 ]
Flanagan, Cormac [2 ]
Yahav, Eran [3 ]
Sagiv, Mooly [1 ]
机构
[1] Tel Aviv Univ, IL-69978 Tel Aviv, Israel
[2] Univ California, Santa Cruz, CA USA
[3] IBM Corp, Thomas J Watson Res Ctr, Box 218, Yorktown Hts, NY 10598 USA
来源
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Verifying concurrent programs is challenging since the number of thread interleavings that need to be explored can be huge even for moderate programs. We present a cartesian semantics that reduces the amount of nondeterminism in concurrent programs by delaying unnecessary context switches. Using this semantics, we construct a novel dynamic partial-order reduction algorithm. We have implemented our algorithm and evaluate it on a small set of benchmarks. Our preliminary experimental results show a significant potential saving in the number of explored states and transitions.
引用
收藏
页码:95 / +
页数:4
相关论文
共 50 条
  • [1] Bounded Partial-Order Reduction
    Coons, Katherine E.
    Musuvathi, Madanlal
    McKinley, Kathryn S.
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (10) : 833 - 848
  • [2] Stateful dynamic partial-order reduction
    Yi, Xiaodong
    Wang, Ji
    Yang, Xuejun
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 149 - +
  • [3] Stateful dynamic partial-order reduction
    National Laboratory for Parallel and Distributed Processing, Changsha, China
    [J]. Lect. Notes Comput. Sci., 2006, (149-167):
  • [4] Guard-based partial-order reduction
    Alfons Laarman
    Elwin Pater
    Jaco van de Pol
    Henri Hansen
    [J]. International Journal on Software Tools for Technology Transfer, 2016, 18 : 427 - 448
  • [5] Guard-based partial-order reduction
    Laarman, Alfons
    Pater, Elwin
    van de Pol, Jaco
    Hansen, Henri
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (04) : 427 - 448
  • [6] Partial-Order Reduction for GPU Model Checking
    Neele, Thomas
    Wijs, Anton
    Bosnacki, Dragan
    van de Pol, Jaco
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 357 - 374
  • [7] Partial-Order Reduction for Supervisory Controller Synthesis
    van der Sanden, Bram
    Geilen, Marc
    Reniers, Michel
    Basten, Twan
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2022, 67 (02) : 870 - 885
  • [8] Cluster-Based Partial-Order Reduction
    Twan Basten
    Dragan Bošnački
    Marc Geilen
    [J]. Automated Software Engineering, 2004, 11 (4) : 365 - 402
  • [9] Partial-order reduction for general state exploring algorithms
    Bošnackǐki D.
    Leue S.
    Lluch Lafuente A.
    [J]. International Journal on Software Tools for Technology Transfer, 2009, 11 (01) : 39 - 51
  • [10] Dynamic partial-order reduction for model checking software
    Flanagan, C
    Godefroid, P
    [J]. ACM SIGPLAN NOTICES, 2005, 40 (01) : 110 - 121