Zobrazeno 1 - 7
of 7
pro vyhledávání: '"Yuri Meshman"'
Publikováno v:
Computer Languages, Systems & Structures. 47:62-76
We present a new abstract interpretation based approach for automatically verifying concurrent programs running on relaxed memory models. Our approach is based on three key insights: (i) Although the behaviors of relaxed memory models (e.g., TSO and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::947b33e2200e76a465679f6e0debb4ca
https://doi.org/10.1016/j.cl.2016.02.003
https://doi.org/10.1016/j.cl.2016.02.003
Publikováno v:
Programming Languages and Systems ISBN: 9783319898834
ESOP
ESOP
Lamport’s Paxos algorithm is a classic consensus protocol for state machine replication in environments that admit crash failures. Many versions of Paxos exploit the protocol’s intrinsic properties for the sake of gaining better run-time performa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0ac5001b47022a3a6b10829a1b8ef6c2
https://doi.org/10.1007/978-3-319-89884-1_32
https://doi.org/10.1007/978-3-319-89884-1_32
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319737201
VMCAI
VMCAI
Remote Memory Access (RMA) networks are emerging as a promising basis for building performant large-scale systems such as MapReduce, scientific computing applications, and others. To achieve this performance, RMA networks exhibit relaxed memory consi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::92a4f5afc2de6584e97a9bf01f7dea73
https://doi.org/10.1007/978-3-319-73721-8_3
https://doi.org/10.1007/978-3-319-73721-8_3
Publikováno v:
FMCAD
We address the problem of synthesizing efficient and correct synchronization for programs running under the C++ relaxed memory model. Given a finite-state program P and a safety property S such that P satisfies S under a sequentially consistent (SC)
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::556e7bc1e79a711104333da86ad411d9
https://doi.org/10.1109/fmcad.2015.7542261
https://doi.org/10.1109/fmcad.2015.7542261
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783662460801
VMCAI
VMCAI
We present a new abstract interpretation based approach for automatically verifying concurrent programs running on relaxed memory models. Our approach is based on three key insights: i behaviors of relaxed models e.g. TSO and PSO are naturally captur
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::793126b5e6bc1ae4bc60c3e5a2757829
https://doi.org/10.1007/978-3-662-46081-8_25
https://doi.org/10.1007/978-3-662-46081-8_25
Publikováno v:
Static Analysis ISBN: 9783319109350
SAS
SAS
We address the problem of fence inference in infinite-state concurrent programs running on relaxed memory models such as TSO and PSO. We present a novel algorithm that can automatically synthesize the necessary fences for infinite-state programs.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e5c63d499021333e58fa81832c4b31fe
https://doi.org/10.1007/978-3-319-10936-7_15
https://doi.org/10.1007/978-3-319-10936-7_15
Publikováno v:
Static Analysis ISBN: 9783642388552
SAS
SAS
We present a novel approach for predicate abstraction of programs running on relaxed memory models. Our approach consists of two steps.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6eec8dfaafe969a269578c784c73019e
https://doi.org/10.1007/978-3-642-38856-9_7
https://doi.org/10.1007/978-3-642-38856-9_7