Zobrazeno 1 - 10
of 50
pro vyhledávání: '"Petri, Gustavo"'
Autor:
Hsiao, Yao, Nikoleris, Nikos, Khyzha, Artem, Mulligan, Dominic P., Petri, Gustavo, Fletcher, Christopher W., Trippel, Caroline
The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $\mu$SPEC models. Despite the efficacy of this approach, a verification gap between $\mu$SPEC
Externí odkaz:
http://arxiv.org/abs/2409.19478
Autor:
Schiebelbein, Edgard, Hatia, Saalik, Bieniusa, Annette, Petri, Gustavo, Ferreira, Carla, Shapiro, Marc
This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic m
Externí odkaz:
http://arxiv.org/abs/2403.11716
An important property of concurrent objects is whether they support progress -a special case of liveness-guarantees, which ensure the termination of individual method calls under system fairness assumptions. Liveness properties have been proposed for
Externí odkaz:
http://arxiv.org/abs/2107.09930
Designing low-latency cloud-based applications that are adaptable to unpredictable workloads and efficiently utilize modern cloud computing platforms is hard. The actor model is a popular paradigm that can be used to develop distributed applications:
Externí odkaz:
http://arxiv.org/abs/1912.03506
Geo-distributed systems often replicate data at multiple locations to achieve availability and performance despite network partitions. These systems must accept updates at any replica and propagate these updates asynchronously to every other replica.
Externí odkaz:
http://arxiv.org/abs/1903.06560
We study a proof methodology for verifying the safety of data invariants of highly-available distributed applications that replicate state. The proof is (1) modular: one can reason about each individual operation separately, and (2) sequential: one c
Externí odkaz:
http://arxiv.org/abs/1903.02759
Publikováno v:
PaPoC 2018 - 5th W. on Principles and Practice of Consistency for Distributed Data, Apr 2016, Porto, Portugal
Referential integrity (RI) is an important correctness property of a shared, distributed object storage system. It is sometimes thought that enforcing RI requires a strong form of consistency. In this paper, we argue that causal consistency suffices
Externí odkaz:
http://arxiv.org/abs/1803.03482
Autor:
Kogan, Kirill, Menikkumbura, Danushka, Petri, Gustavo, Noh, Youngtae, Nikolenko, Sergey, Eugster, Patrick
Buffering architectures and policies for their efficient management constitute one of the core ingredients of a network architecture. In this work we introduce a new specification language, BASEL, that allows to express virtual buffering architecture
Externí odkaz:
http://arxiv.org/abs/1510.04235
Publikováno v:
EPTCS 89, 2012, pp. 19-33
We propose a novel, operational framework to formally describe the semantics of concurrent programs running within the context of a relaxed memory model. Our framework features a "temporary store" where the memory operations issued by the threads are
Externí odkaz:
http://arxiv.org/abs/1208.5915
Publikováno v:
[0] LIP6, Sorbonne Université, Inria, Paris, France; Arm Research, Cambridge, UK. 2020
[Other] LIP6, Sorbonne Université, Inria, Paris, France; Arm Research, Cambridge, UK. 2020
[Other] LIP6, Sorbonne Université, Inria, Paris, France; Arm Research, Cambridge, UK. 2020
To provide high availability in distributed systems, object replicas allow concurrent updates. Although replicas eventually converge, they may diverge temporarily, for instance when the network fails. This makes it difficult for the developer to reas
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::ee8f6d6d32a4682b343b0e50ffd32590
https://hal.science/hal-02492599/file/esop2020.pdf
https://hal.science/hal-02492599/file/esop2020.pdf