微信服务号

微信订阅号

2025-4-11- 17
Home > Archive>Volume 32, Issue 6, 2021 >1612-1630. DOI:10.13328/j.cnki.jos.006240
PDF HTML XML Export Cite reminder
Reverse Unfolding of Petri Nets and its Application in Program Data Race Detection
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61602279,61472229); National Key Research and Development Plan (2016YFC0801406); Taishan Scholars Program of Shandong Province (ts20190936); Excellent Youth Innovation Team Foundation of Shandong Higher School (2019KJN024); Postdoctoral Innovation Foundation of Shandong Province (201603056); Shandong-Chongqing Science and Technology Cooperation Plan (cstc2020jscx-lyjsAX0008); Open Foundation of First Institute of Oceanography, MNR (2018002); Shandong University of Science and Technology Research Fund (2015TDJH102)

  • Article
    • | |
  • Metrics
    • |
  • Reference [34]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Unfolding technology can partially alleviate the state explosion problem in Petri net through branching processes. However, an unfolding still contains all states of a system. Some practical problems only need to determine the coverability of a specific state, which is expected to reduce the scale of unfolding net. This study proposes a target-oriented reverse unfolding algorithm for the coverability problem of 1-safe Petri nets, which combines heuristic technology to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding technology is applied to the formal verification of concurrent programs, and the data race detection problem is converted into the coverability problem of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward unfolding and reverse unfolding in the coverability problem of Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.

    Reference
    [1] Han L, Xing K, Chen X, Xiong F. A Petri net-based particle swarm optimization approach for scheduling deadlock-prone flexible manufacturing systems. Journal of Intelligent Manufacturing, 2018,29(5):1083-1096. https://doi.org/10.1007/s10845-015-1161-2
    [2] Hu L, Liu Z, Hu W, Wang Y, Tan J, Wu F. Petri-Net-Based dynamic scheduling of flexible manufacturing system via deep reinforcement learning with graph convolutional network. Journal of Manufacturing Systems, 2020,55:1-4. https://doi.org/10.1016/j.jmsy.2020.02.004
    [3] Fauzan AC, Sarno R, Yaqin MA. Performance measurement based on coloured Petri net simulation of scalable business processes. In:Proc. of the 20174th Int'l Conf. on Electrical Engineering, Computer Science and Informatics (EECSI). IEEE, 2017. 1-6. https://doi.org/10.1109/EECSI.2017.8239121
    [4] Liu C, Zeng Q, Duan H, Wang L, Tan J, Ren C, Yu W. Petri net based data-flow error detection and correction strategy for business processes. IEEE Access, 2020,8:43265-43276. https://doi.org/10.1109/ACCESS.2020.2976124
    [5] Lu F, Tao R, Du Y, Zeng Q, Bao Y. Deadlock detection-oriented unfolding of unbounded Petri nets. Information Sciences, 2019, 497:1-22. https://doi.org/10.1016/j.ins.2019.05.021
    [6] Xiang D, Liu G, Yan C, Jiang C. Detecting data inconsistency based on the unfolding technique of petri nets. IEEE Trans. on Industrial Informatics, 2017,13(6):2995-3005. https://doi.org/10.1109/TII.2017.2698640
    [7] McMillan KL. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 1992. 164-177.
    [8] Engelfriet J. Branching processes of Petri nets. Acta Informatica, 1991,28(6):575-591. https://doi.org/10.1007/BF01463946
    [9] Esparza J, Römer S, Vogler W. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 2002, 20(3):285-310. https://doi.org/10.1023/A:1014746130920
    [10] Khomenko V, Koutny M, Vogler W. Canonical prefixes of Petri net unfoldings. Acta Informatica, 2003,40(2):95-118. https://doi. org/10.1007/s00236-003-0122-y
    [11] Heljanko K, Khomenko V, Koutny M. Parallelisation of the Petri net unfolding algorithm. In:Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg:Springer-Verlag, 2002. 371-385. https://doi.org/10.1007/3-540-46002-0_26
    [12] Benito FC, Kunzle LA. Unfolding for time Petri net. IEEE Latin America Transactions, 2017,15(5):1001-1008. https://doi.org/10.1109/TLA.2017.7912599
    [13] Schwarick M, Rohr C, Liu F, Assaf G, Chodak J, Heiner M. Efficient unfolding of coloured Petri nets using interval decision diagrams. In:Proc. of the Int'l Conf. on Applications and Theory of Petri Nets and Concurrency. Cham:Springer-Verlag, 2020. 324-344. https://doi.org/10.1007/978-3-030-51831-8_16
    [14] Dong L, Liu G, Xiang D. Verifying CTL with unfoldings of Petri nets. In:Proc. of the Int'l Conf. on Algorithms and Architectures for Parallel Processing. Cham:Springer-Verlag, 2018. 47-61. https://doi.org/10.1007/978-3-030-05063-4_5
    [15] Liu G, Reisig W, Jiang C, Zhou M. A branching-process-based method to check soundness of workflow systems. IEEE Access, 2016,4:4104-4118. https://doi.org/10.1109/ACCESS.2016.2597061
    [16] Chatain T, Paulevé L. Goal-Driven unfolding of Petri nets. arXiv preprint arXiv:1611.01296, 2016.
    [17] Bonet B, Haslum P, Hickmott S, Thiébaux S. Directed unfolding of Petri nets. In:Proc. of the Trans. on Petri Nets and Other Models of Concurrency I. Berlin, Heidelberg:Springer-Verlag, 2008. 172-198. https://doi.org/10.1007/978-3-540-89287-8_11
    [18] Bonet B, Haslum P, Khomenko V, Thiébaux S, Vogler W. Recent advances in unfolding technique. Theoretical Computer Science, 2014,551:84-101. https://doi.org/10.1016/j.tcs.2014.07.003
    [19] Abdulla PA, Iyer SP, Nylén A. SAT-Solving the coverability problem for Petri nets. Formal Methods in System Design, 2004,24(1):25-43. https://doi.org/10.1023/B:FORM.0000004786.30007.f8
    [20] Leveson NG, Turner CS. An investigation of the Therac-25 accidents. Computer, 1993,26(7):18-41. https://doi.org/10.1109/MC.1993.274940
    [21] Poulsen K. Software bug contributed to blackout. Security Focus. 2004. http://www.securityfocus.com/news/8016
    [22] Joab J. Nasdaq's Facebook glitch came from ‘race conditions’. 2012. http://www.computerworld.com/s/article/9227350
    [23] Blackshear S, Gorogiannis N, O'Hearn PW, Sergey I. RacerD:Compositional static race detection. Proc. of the ACM on Programming Languages, 2018.2(OOPSLA):1-28. https://doi.org/10.1145/3276514
    [24] Chatarasi P, Shirako J, Kong M, Sarkar V. An extended polyhedral model for SPMD programs and its use in static data race detection. In:Proc. of the Int'l Workshop on Languages and Compilers for Parallel Computing. Cham:Springer-Verlag, 2016. 106-120. https://doi.org/10.1007/978-3-319-52709-3_10
    [25] Bora U, Das S, Kukreja P, Joshi S, Upadrasta R, Rajopadhye S. Llov:A fast static data-race checker for OpenMP programs. ACM Trans. on Architecture and Code Optimization (TACO), 2020,17(4):1-26. https://doi.org/10.1145/3418597
    [26] Wilcox JR, Flanagan C, Freund SN. VerifiedFT:A verified, high-performance precise dynamic race detector. In:Proc. of the 23rd ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming. 2018. 354-367. https://doi.org/10.1145/3178487.3178514
    [27] Gu Y, Mellor-Crummey J. Dynamic data race detection for OpenMP programs. In:Proc. of the SC18:Int'l Conf. for High Performance Computing, Networking, Storage and Analysis. IEEE, 2018. 767-778. https://doi.org/10.1109/SC.2018.00064
    [28] Lidbury C, Donaldson AF. Dynamic race detection for C++11. ACM SIGPLAN Notices, 2017,52(1):443-457. https://doi.org/10.1145/3093333.3009857
    [29] Kavi KM, Moshtaghi A, Chen DJ. Modeling multithreaded applications using Petri nets. Int'l Journal of Parallel Programming, 2002,30(5):353-371. https://doi.org/10.1023/A:1019917329895
    [30] Vallée-Rai R, Co P, Gagnon E, Hendren L, Lam P, Sundaresan V. Soot:A Java bytecode optimization framework. In:Proc. of the CASCON 1st Decade High Impact Papers. 2010. 214-224. https://doi.org/10.1145/1925805.1925818
    [31] https://github.com/Zongyin-Hao/Coverability
    [32] Liu GJ. Meta-unfolding of Petri Nets:A Model Checking Method of Concurrent Systems. Beijing:Science Press, 2020(in Chinese).
    附中文参考文献:
    [32] 刘关俊.Petri网的元展:一种并发系统模型检测方法.北京:科学出版社,2020.
    Related
    Cited by
Get Citation

郝宗寅,鲁法明. Petri网的反向展开及其在程序数据竞争检测的应用.软件学报,2021,32(6):1612-1630

Copy
Share
Article Metrics
  • Abstract:1986
  • PDF: 4720
  • HTML: 3398
  • Cited by: 0
History
  • Received:August 31,2020
  • Revised:October 26,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034574Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063