Detalhes
Nome
Paulo Sérgio AlmeidaCargo
Investigador SéniorDesde
01 novembro 2011
Nacionalidade
PortugalCentro
Laboratório de Software ConfiávelContactos
+351253604440
paulo.s.almeida@inesctec.pt
2025
Autores
Almeida, PS;
Publicação
ACM COMPUTING SURVEYS
Abstract
Conflict-free Replicated Data Types (CRDTs) allow optimistic replication in a principled way. Different replicas can proceed independently, being available even under network partitions and always converging deterministically: Replicas that have received the same updates will have equivalent state, even if received in different orders. After a historical tour of the evolution from sequential data types to CRDTs, we present in detail the two main approaches to CRDTs, operation-based and state-based, including two important variations, the pure operation-based and the delta-state based. Intended for prospective CRDT researchers and designers, this article provides solid coverage of the essential concepts, clarifying some misconceptions that frequently occur, but also presents some novel insights gained from considerable experience in designing both specific CRDTs and approaches to CRDTs.
2025
Autores
Kassam, Z; Almeida, PS; Shoker, A;
Publicação
IEEE Access
Abstract
TCP is the default transport protocol of choice, namely for message-oriented middleware protocols (e.g., ZMTP, AMQP, MQTT) or distributed language runtimes (e.g., distributed Erlang), where exactly-once (EO) messaging is paramount. However, EO is only guaranteed within the TCP session, since reality shows that TCP connections can fail under many circumstances. Ensuring EO delivery ends up at the middleware layer, at the cost of higher complexity and lack of obliviouness - due to the use of permanent per-peer state. Moreover, using TCP at scale in highly concurrent systems leads to the need for TCP connection multiplexing, and possibly drastic performance loss due to head-of-line blocking. This paper introduces Exon, an oblivious exactly-once messaging protocol, and a corresponding lightweight library implementation over UDP. Exon uses a novel strategy of a per-message four-way protocol to ensure oblivious exactly-once messaging, with on-demand protocol-level "soft half-connections", established when needed and safely discarded. Exon achieves simultaneously: correctness with no timing assumptions, obliviousness, and performance through merging and pipelining basic protocol messages. Exon also employs a reliable delegation technique to handover the sending responsibility to a mediating node, without violating EO, when the sender the receiver are directly unreachable to each other and even if the message had already been delivered. The empirical evaluation of Exon demonstrates significant improvements over TCP in throughput and latency under packet loss, while maintaining a negligible overhead in healthy networks. © 2013 IEEE.
2024
Autores
Almeida, PS; Shapiro, E;
Publicação
CoRR
Abstract
2024
Autores
Almeida, PS;
Publicação
CoRR
Abstract
2023
Autores
Barros, M; Ramos, M; Gomes, A; Cunha, A; Pereira, J; Almeida, PS;
Publicação
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2023
Abstract
Automatic grading based on unit tests is a key feature of massive open online courses (MOOC) on programming, as it allows instant feedback to students and enables courses to scale up. This technique works well for sequential programs, by checking outputs against a sample of inputs, but unfortunately it is not adequate for detecting races and deadlocks, which precludes its use for concurrent programming, a key subject in parallel and distributed computing courses. In this paper we provide a hands-on evaluation of verification and testing tools for concurrent programs, collecting a precise set of requirements, and describing to what extent they can or can not be used for this purpose. Our conclusion is that automatic grading of concurrent programming exercises remains an open challenge.
Teses supervisionadas
2023
Autor
Ziad Ali Kassam
Instituição
UM
2022
Autor
Ricardo Oliveira Vaz
Instituição
UM
2022
Autor
Ziad Ali Kassam
Instituição
UM
2021
Autor
Ziad Ali Kassam
Instituição
UM
2021
Autor
Ziad Ali Kassam
Instituição
UM
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.