A Separation Logic for Concurrent Randomized Programs

被引：28
作者：
Tassarotti, Joseph [1 ]
Harper, Robert [1 ]
机构：
[1] Carnegie Mellon Univ, Comp Sci Dept, Pittsburgh, PA 15213 USA
来源：
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2019年 / 3卷 / POPL期
关键词：
separation logic; concurrency; probability;
D O I：
10.1145/3290377
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.
引用
收藏
页数：30
相关论文
共 67 条
  • [11] Beck J. M., 1969, LECT NOTES MATH, P119
  • [12] Simple relational correctness proofs for static analyses and program transformations
    Benton, N
    [J]. ACM SIGPLAN NOTICES, 2004, 39 (01) : 14 - 25
  • [13] Bizjak Ales, 2015, FDN SOFTW SCI COMP S FDN SOFTW SCI COMP S
  • [14] Boyd-Wickizer Silas., 2010, P 9 USENIX C OPERATI, P1
  • [15] Boyland J, 2003, LECT NOTES COMPUT SC, V2694, P55
  • [16] Chlipala Adam., 2017, Certified Programming with Dependent Types
  • [17] Dice Dave, 2013, 25 ACM S PAR ALG ARC, P43, DOI 10.1145/2486159.2486182
  • [18] DIJKSTRA EW, 1975, COMMUN ACM, V18, P453, DOI [10.1145/360933.360975, 10.1145/390016.808417]
  • [19] Dinsdale-Young T., 2013, POPL
  • [20] Dinsdale-Young T, 2010, LECT NOTES COMPUT SC, V6183, P504, DOI 10.1007/978-3-642-14107-2_24
1234567