Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Paulo Sérgio Almeida
  • Cargo

    Investigador Sénior
  • Desde

    01 novembro 2011
001
Publicações

2025

Approaches to Conflict-free Replicated Data Types

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

Exon: An Oblivious Exactly-Once Messaging Protocol With Reliable Delegation

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

The Blocklace: A Universal, Byzantine Fault-Tolerant, Conflict-free Replicated Data Type

Autores
Almeida, PS; Shapiro, E;

Publicação
CoRR

Abstract

2024

A Framework for Consistency Models in Distributed Systems

Autores
Almeida, PS;

Publicação
CoRR

Abstract

2023

An Experimental Evaluation of Tools for Grading Concurrent Programming Exercises

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

Beyong Distributed Transctions through Exactly-once Exchanges

Autor
Ziad Ali Kassam

Instituição
UM

2022

Sistema de pagamentos descentralizado para e-commerce na Blockchain

Autor
Ricardo Oliveira Vaz

Instituição
UM

2022

Beyong Distributed Transctions through Exactly-once Exchanges

Autor
Ziad Ali Kassam

Instituição
UM

2021

Beyong Distributed Transctions through Exactly-once Exchanges

Autor
Ziad Ali Kassam

Instituição
UM

2021

Beyond Distributed Transactions through Exactly-once Exchanges

Autor
Ziad Ali Kassam

Instituição
UM