Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Carl Leonardsson"'
Autor:
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, Yunyun Zhu
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instructio
Externí odkaz:
https://doaj.org/article/312a3fcfaf2148e288118a8328f83217
Publikováno v:
IEEE Transactions on Parallel and Distributed Systems. 28:3413-3425
Cache coherence protocols based on self-invalidation allow simpler hardware implementation compared to traditional write-invalidation protocols, by relying on data-race-free semantics and applying self-invalidation on synchronization points. Their si
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d74840ca1b3d6dd4b618ce53e373c18
https://doi.org/10.1109/tpds.2017.2720744
https://doi.org/10.1109/tpds.2017.2720744
Autor:
Carl Leonardsson, Alberto Ros, Mohamed Faouzi Atig, Yunyun Zhu, Stefanos Kaxiras, Parosh Aziz Abdulla
Publikováno v:
Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783319395692
FORTE
FORTE
Cache coherence protocols using self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1297549a6e1f2d6b47d514b53cd32961
https://doi.org/10.1007/978-3-319-39570-8_2
https://doi.org/10.1007/978-3-319-39570-8_2
Publikováno v:
Computer Aided Verification ISBN: 9783319415390
CAV (2)
CAV (2)
We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme f
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8bd066eff44d9bfd5f11fd6ff69f6f77
https://doi.org/10.1007/978-3-319-41540-6_8
https://doi.org/10.1007/978-3-319-41540-6_8
Autor:
Mohamed Faouzi Atig, Konstantinos Sagonas, Stavros Aronis, Carl Leonardsson, Parosh Aziz Abdulla, Bengt Jonsson
We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Ch
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::23ba1f197614b769a2a259e3cc2a9058
http://arxiv.org/abs/1501.02069
http://arxiv.org/abs/1501.02069
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642367410
TACAS
TACAS
We introduce Memorax, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-tr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a082d0262789c18417f3a9f4d5ab6cc2
https://doi.org/10.1007/978-3-642-36742-7_37
https://doi.org/10.1007/978-3-642-36742-7_37
Publikováno v:
Static Analysis ISBN: 9783642331244
SAS
SAS
We propose an automatic fence insertion and verification framework for concurrent programs running under relaxed memory. Unlike previous approaches to this problem, which allow only variables of finite domain, we target programs with (unbounded) inte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::69b165a6ff2d34262340147b61b3dcfb
https://doi.org/10.1007/978-3-642-33125-1_13
https://doi.org/10.1007/978-3-642-33125-1_13
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642287558
TACAS
TACAS
We give a sound and complete fence insertion procedure for concurrent finite-state programs running under the classical TSO memory model. This model allows "write to read" relaxation corresponding to the addition of an unbounded store buffer between
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3cd371c6b143922c3b9765c67928d6b9
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-175078
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-175078