Opportunistic Monitoring of Multithreaded Programs

被引:1
作者
Soueidi, Chukri [1 ]
El-Hokayem, Antoine [1 ]
Falcone, Ylies [1 ]
机构
[1] Univ Grenoble Alpes, LIG, INRIA, CNRS,Grenoble INP, F-38000 Grenoble, France
来源
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, FASE 2023 | 2023年 / 13991卷
关键词
RUNTIME VERIFICATION; MEMORY; ATOMICITY;
D O I
10.1007/978-3-031-30826-0_10
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We introduce a generic approach for monitoring multithreaded programs online leveraging existing runtime verification (RV) techniques. In our setting, monitors are deployed to monitor specific threads and only exchange information upon reaching synchronization regions defined by the program itself. They use the opportunity of a lock in the program, to evaluate information across threads. As such, we refer to this approach as opportunistic monitoring. By using the existing synchronization, our approach reduces additional overhead and interference to synchronize at the cost of adding a delay to determine the verdict. We utilize a textbook example of readers-writers to show how opportunistic monitoring is capable of expressing specifications on concurrent regions. We also present a preliminary assessment of the overhead of our approach and compare it to classical monitoring showing that it scales particularly well with the concurrency present in the program.
引用
收藏
页码:173 / 194
页数:22
相关论文
共 57 条
[1]   Shared memory consistency models: A tutorial [J].
Adve, SV ;
Gharachorloo, K .
COMPUTER, 1996, 29 (12) :66-&
[2]  
Agarwal A., 2005, Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing. PODC05, P19, DOI [DOI 10.1145/1073814.1073818, 10.1145/1073814.1073818]
[3]  
AHAMAD M, 1995, DISTRIB COMPUT, V9, P37, DOI 10.1007/BF01784241
[4]   Adding trace matching with free variables to AspectJ [J].
Allan, C ;
Avgustinov, P ;
Christensen, AS ;
Hendren, L ;
Kuzins, S ;
Lhoták, O ;
de Moor, O ;
Sereni, D ;
Sittampalam, G ;
Tibble, J .
ACM SIGPLAN NOTICES, 2005, 40 (10) :345-364
[5]  
[Anonymous], Patterns in property specications for nite-state verication home page
[6]  
[Anonymous], 2000, ACM 2000 JAV GRAND C, DOI DOI 10.1145/337449.337465
[7]  
Barringer Howard, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P68, DOI 10.1007/978-3-642-32759-9_9
[8]  
Bartocci Ezio, 2018, Lectures on Runtime. Verification Introductory and Advanced Topics. LNCS 10457, P1, DOI 10.1007/978-3-319-75632-5_1
[9]  
Bartocci E., 2017, International Journal on Software Tools for Technology Transfer