Bounded verification of message-passing concurrency in Go using Promela and Spin

被引：10

作者：

Dilley, Nicolas ^{[1
]}

Lange, Julien ^{[1
]}

机构：

[1] Univ Kent, Canterbury, Kent, England

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2020年 / 314期

关键词：

D O I：

10.4204/EPTCS.314.4

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or behavioural types, are encoded in Promela, hence can be efficiently verified with Spin. We improve on previous works by verifying programs that include communication-related parameters that are unknown at compile-time, i.e., programs that spawn a parameterised number of threads or that create channels with a parameterised capacity. These programs are checked via a bounded verification approach with bounds provided by the user.

引用

页码：34 / 45

页数：12

共 50 条

[31] Message-Passing Algorithms for Channel Estimation and Decoding Using Approximate Inference
Badiu, Mihai-A
Kirkelund, Gunvor E.
Manchon, Carles Navarro
Riegler, Erwin
Fleury, Bernard H.
2012 IEEE INTERNATIONAL SYMPOSIUM ON INFORMATION THEORY PROCEEDINGS (ISIT), 2012,
[32] FORECASTING SPARSE TRAFFIC CONGESTION PATTERNS USING MESSAGE-PASSING RNNS
Iyer, Shiva R.
An, Ulzee
Subramanian, Lakshminarayanan
2020 IEEE INTERNATIONAL CONFERENCE ON ACOUSTICS, SPEECH, AND SIGNAL PROCESSING, 2020, : 3772 - 3776
[33] INFERENCE OF GENE-REGULATORY NETWORKS USING MESSAGE-PASSING ALGORITHMS
Shamaiah, Manohar
Lee, Sang Hyun
Vikalo, Haris
2010 IEEE INTERNATIONAL WORKSHOP ON GENOMIC SIGNAL PROCESSING AND STATISTICS (GENSIPS), 2010,
[34] Sparse Code Multiple Access Decoding Using Message-Passing Algorithm
Andhary, Lathifa Rizqi
Nuha, Hilal H.
Haryanti, Tita
2022 INTERNATIONAL CONFERENCE ON DATA SCIENCE AND ITS APPLICATIONS (ICODSA), 2022, : 161 - 165
[35] Identifying influential subpopulations in metapopulation epidemic models using message-passing theory
Choi, Jeehye
Min, Byungjoon
PHYSICAL REVIEW E, 2022, 105 (04)
[36] Optimizing Message-Passing on Multicore Architectures using Hardware Multi-Threading
Buono, Daniele
De Matteis, Tiziano
Mencagli, Gabriele
Vanneschi, Marco
2014 22ND EUROMICRO INTERNATIONAL CONFERENCE ON PARALLEL, DISTRIBUTED, AND NETWORK-BASED PROCESSING (PDP 2014), 2014, : 262 - 270
[37] High Performance Computing of Gene Regulatory Networks using a Message-Passing Model
Glass, Kimberly
Quackenbush, John
Kepner, Jeremy
2015 IEEE HIGH PERFORMANCE EXTREME COMPUTING CONFERENCE (HPEC), 2015,
[38] Scalable CFD computations using message-passing and distributed shared memory algorithms
Plazek, J
Banas, K
Kitowski, J
RECENT ADVANCES IN PARALLEL VIRTUAL MACHINE AND MESSAGE PASSING INTERFACE, PROCEEDINGS, 2000, 1908 : 282 - 288
[39] Performance of message-passing systems using a zero-copy communication protocol
Melas, P
Zaluska, EJ
1998 INTERNATIONAL CONFERENCE ON PARALLEL ARCHITECTURES AND COMPILATION TECHNIQUES, PROCEEDINGS, 1998, : 264 - 271
[40] A Message-Passing Architecture Without Public Ids using Send-to-Behavior
Wang, Eric Shing-Suan
Dang, Zhe
2015 30TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2015, : 902 - 905

← 1 2 3 4 5 →