Implementing, Verifying and Debugging Distributed Systems
Elisa Gonzalez Boix
https://soft.vub.ac.be/disco/

How it all started?
•2

A programming model for ubiquitous computing
In an ubiquitous context,
asynchronous communication suits
better, why don’t you implement anactor-based language?
my own language?!?

Ubiquitous Computing
Vision (1988)

Jessie Dedecker

Actors in JavaPic%

3

factor(n): createActor ({fac (c, client)::{if ( n> 1, {next: factor(n-1);
if( n = c, next.fac(c, client),next.fac( c*n, client))},client.result(c) )}});
factorial : createActor({result(res):: { display(res)};
compute(num):: {a : factor(num);a.fac (num, thisActor())}});
factorial.compute(3);(Industry)

How it all started again?
•5a programming model for ubiquitous computing
what about exploring afailure handling model for
AmbientTalk?
TheoD’hondt

Wolfgang
De Meuter

JessieDedeckerTom
Van Cutsem

AmbientTalk?

Stijn
Mostinckx

J. Dedecker, T. Van Cutsem, S. Mostinckx, T. D'Hondt, W. De Meuter. 2006. Ambient-Oriented Programming in AmbientTalk. In Proceedings of the 20th European
Conference on Object-Oriented Programming (ECOOP), LNCS Vol. 4067, pp. 230-254, Springer-Verlag.”, 2006.

AmbientTalk’s Distributed Model = OO + Events

6

A superset of object-oriented programming that is explicitly geared towards programming
distributed applications that run on mobile ad hoc networks
Generate and receive
application requests

obj<-msg(arg)def msg(param) { ... }Follow-up on
outstanding requests

when: future becomes: { |result| ... }React to services appearing
and disappearing

when: type discovered: { |ref| ... }whenever: type discovered: { |ref| ... }React to references
disconnecting,reconnecting

when: ref disconnected: { ... }when: ref reconnected: { ... }whenever: ref disconnected: { ... }whenever: ref reconnected: { ... }Tom Van Cutsem, Stijn Mostinckx, Elisa Gonzalez Boix, Jessie Dedecker, and Wolfgang De Meuter. Ambienttalk: object-oriented event-driven programming in
mobile ad hoc networks. In Inter. Conf. of the Chilean Computer Science Society (SCCC), pages 3–12. IEEE Computer Society, 2007.

Distributed Applications in AmbientTalk

deftype PingPong;

deftype PingPong;def pingPong := object: {def ping(){system.println(“received ping");`pong;}};

whenever: PingPong
discovered: {|farRef|
when: farRef<-ping()@FutureMessage()
becomes: {|val|system.println("received " + val);}}export: pingPong as: PingPong;•

https://soft.vub.ac.be/amop/

Data stored at the owner, and all operations go via asynchronous message
passing7

How to reconcile failures with distributed event-based model?
“A lease denotes the right to access a resource for a speci cduration negotiated when the access is rst requested.”lease: 10.minutes
sessiondisconnect

Connected

Disconnected(messages areforwarded)(messages arebuffered)

when: ref disconnected: { ... }when: ref reconnected: { ... }when: ref expired: { ... }reconnect
expireexpirewhenever: ref disconnected: { ... }whenever: ref reconnected: { ... }Expiredfifi(messages aredropped)

8

Distributed P2P applications

9Urbi ock

WeScribble

PortalPong

WePongfl

http://tinyurl.com/ambienttalkyoutube

WePokerMany times data needed to be shared…

102021
def counter := isolate: {def val := 0;
def incr(){ val := val + 1 };def decr(){ val := val - 1 };def value(){ val };};

increasing availability: operations
can execute locally
improving reliability: avoid single
points of failure.

providing some form ofconsistency is left to theapplication programmer

Could we build replicated objects so that ..
developers can customize con ict resolution
according to the application's needs

fl•

11

Could we build replicated objects so that ..
developers can customize con ict resolution
according to the application's needs•

without exposing them to merge procedures

fl•

12

Replicated Data Types (RDTs)

Shapiro et al. 201113

Replicated Data Types (RDTs)

14

RDT
def statedBasedCounter := object: {def vInc;def myId;

Shapiro et al. 2011

def init(typeName,id,n) { .. };def increment() {def val := vInc.at(myId);
vInc.atPut(myId, val +1);};
def value() {def res := 0;
vInc.each: { |val|
res := res + val };res};
def merge(senderVector) {def i := 0;
vInc.each: { |a|def b := senderVector.get(i);vInc.atPut(i, Math.max(a,b));i := i + 1}};
… };

Replicated Data Types (RDTs)

15

RDT Distribution aspects
def statedBasedCounter := object: {import CRDTModule.CRDTTrait;
def vInc;def myId;

Shapiro et al. 2011

def init(typeName,id,n) { .. };def increment() {def val := vInc.at(myId);
vInc.atPut(myId, val +1);};
def value() {def res := 0;
vInc.each: { |val|
res := res + val };res};
def merge(senderVector) {def i := 0;
vInc.each: { |a|def b := senderVector.get(i);vInc.atPut(i, Math.max(a,b));i := i + 1}};
… };def CRDTTrait := object: {def typeName := defaultCRDT;
def replicas := [];def sync(){
self.broadcast(<-merge(self.serialize()));};
def broadcast(msg) {self.replicas.each: { |farRef|
farRef <+ msg}};
def goOnline(){export: self as: (self.typeName);
whenever: (self.typeName) discovered: {| farRef |self.replicas := self.replicas + [farRef];}}};Could we build replicated data types that..
16•

are application-speci c ?
•customize concurrency semantics to the application needs

support application invariants?

•are correct out-of-the box?

•

can be arbitrarily composed?

•

can be applied to dynamic environments with memory and network
constraints?
fi•

ECROsSimplifying the development of application-speci c RDTs

fi

Kevin De Porre, Carla Ferreira, Nuno Preguiça, and Elisa Gonzalez Boix. 2021. ECROs: building global scale systems from sequential code.
Proc. ACM Program. Lang. 5, OOPSLA, Article 107 (October 2021), 30 pages. https://doi.org/10.1145/3485484

Explicitly Consistent Replicated Object (ECRO)•General approach for building hybrid RDTs

Distributed
Specification

sequential
data type•

Replicated data type

Avoids unnecessary coordination
Fast when possible (EC)consistent when needed (SC)18

Explicitly Consistent Replicated Object (ECRO)•General approach for building hybrid RDTs
sequential
data type
Distributed
Specification

Replicated data type

Fast when possible (EC)consistent when needed (SC)19

Building Geo-Distributed Apps, the ECRO Way
Implementing an Add-Wins Set
Sequential implementation in Scala

20

Building Geo-Distributed Apps, the ECRO Way
Implementing an Add-Wins Set

fi

Sequential implementation in ScalaDSL for distributed speci cation

21

Building Geo-Distributed Apps, the ECRO Way
sni
Wev
Remo

Implementing an Add-Wins Set

22

DSL for distributed speci cation

Sequential implementation in ScalaremovefinotBuilding Geo-Distributed Apps, the ECRO Way

23

ECRO Data Type
Replicated Data Type

Sequential implementation

Translation

DSL for distributed speci cationOrdana
Analysis Toolfi

SMT SolverOrdana: Statically Analyzes Distributed Specs
Derives information about:
1. Commutative methods

2. Con icting methods
And nds:
3. Coordination-free solutions to con icts

flfifl

4. Fine-grained locks if no solution can be found24

Serializing Operations: the ECRO Algorithm• Replicas serialize operations locally• strong convergence• invariant preservation (i.e. safety)
Machine 1

Machine 2
Replicated Objects

Replicated Objects

Add-Wins Set Replica

Add-Wins Set Replica

Object’s State

Object State5128175

ECRO Replication Algorithmhbhb
co128

ECRO Replication Algorithm
Method call
Propagation

hbhb
co1725

Validation

26

Portfolio of ECROs
Performanceof ECROs vs PoR and RedBlue consistency

fi

ECRO
PoRRedBlue

1500

1000500n
eA
uc
tio
os
clid
plac

eB

r
U
erst
gi
re

uy
N
eB
orst

seow

n
tio
en
Auc
op

St

atus

0get

Latency (in ms)

Well-known CRDTs
Counter
EW-Flag
DW-Flag
AW-SetRW-Set
AW-Map
RW-MapList
No CRDT
StackQueue
Application Speci c
RUBiSECROs: Take Aways

27•Augment sequential DT with distributed speci cation•

Static analysis is key to derive ef cient RDTs•

But… separate speci cation•fi•

in FOL —> non-trivial, error-prone
subtle errors —> runtime anomalies
must evolve along with the codefi•fi•allows for informed decision at runtime

How to ease the development of ECROs?
•High-level OOP language for sequential DTs•

De ne concurrency semantics and invariants•

Fully compilable to SMT—> FOL speci cations for freefifi• Synthesizes ECROs28

The EFx language29EFx
implementation
concurrency contract

Analyzer
EFx AST
SMT-LIB analysis
code

OrdanaRDTinfoEFx ASTEFx
sourcecode

parseanalyze
ECRO

transpileCompiler
SMT plugin

JS plugin

Scala plugin...

ScalaPgm

Add-Wins Set in EFx
trait SetOps[V] {val set: Set[V]protected def copy(set: Set[V]): SetOps[V]def contains(elem: V) = this.set.contains(elem)
def add(elem: V)= this.copy(this.set.add(elem))def remove(elem: V)= this.copy(this.set.remove(elem))}@replicatedclass AWSet[V](set: Set[V]) extends SetOps[V] {protected def copy(set: Set[V]) =new AWSet(set)// add wins
inv add(elem: V) {this.contains(elem)}}30Remove-Wins Set in EFx

31

trait SetOps[V] {val set: Set[V]protected def copy(set: Set[V]): SetOps[V]def contains(elem: V) = this.set.contains(elem)
def add(elem: V)= this.copy(this.set.add(elem))def remove(elem: V)= this.copy(this.set.remove(elem))}@replicatedclass AWSet[V](set: Set[V]) extends SetOps[V] {protected def copy(set: Set[V]) =new AWSet(set)@replicatedclass RWSet[V](set: Set[V]) extends SetOps[V] {protected def copy(set: Set[V]) =new RWSet(set)// add wins
inv add(elem: V) {this.contains(elem)}}// remove wins
inv remove(elem: V) {!this.contains(elem)}}Validation: Portfolio of RDTs

ECRO portfolio

Application speci cfi32

VeriFx
Correct replicated data types for the masses

Kevin De Porre, Carla Ferreira, and Elisa Gonzalez Boix. VeriFx: Correct replicated data types for the masses. In 37th European Conference
on Object-Oriented Programming, ECOOP 2023, pages 9:1--9:45. Schloss Dagstuhl, July 2023.

The VeriFx Language

High-level OOP language with extensive functional collections•Features a novel proof construct•••used by programmers
describe application-speci ccorrectness properties

Also fully compilable to SMT—> Automated proof veri cationfi•maps, sets, vectors, etc.

fi•

http://verifx.org/34

VeriFx’s Iterative Work ow for developing RDTs

Design RDT
Implement RDT in VeriFx
Automated veriﬁcation

Modify RDTimplementation

correct?
noflInterpret
counterexample

yesTranspile
Deploy insystem

http://verifx.org/

35

Supporting development of distributed systems goes beyond
providing novel programming models

Tooling is essential!

37

Reasoning about distributed events..

Generate and receive
application requests

obj<-msg(arg)def msg(param) { ... }Follow-up on
outstanding requests

when: future becomes: { |result| ... }React to services appearing when: type discovered: { |ref| ... }and disappearing
whenever: type discovered: { |ref| ... }React to references
disconnecting,reconnecting, andexpiring

when: ref disconnected: { ... }when: ref reconnected: { ... }when: ref expired: { ... }whenever: ref disconnected: { ... }whenever: ref reconnected: { ... }Elisa Gonzalez Boix, Carlos Noguera, and Wolfgang De Meuter. Distributed debugging for mobile networks. Journal of Systems andSoftware, 90:76–90, 2014.

38

REME-D Breakpoint Catalog
ints
akpo

oin

ts

Me
ssa
ge
resolut

ion

39

ts

kp
reandcobr

oin

na

itio

oin
kp
ea

so
rets

br

lut
ion

ts

oin

kp
ea
brlbearekp

Message resolution breakpoint

RoleDesignation

Objective

Sender breakpoints
Receiver breakpoints
Code breakpoints
Conditional breakpoints
On entry breakpoints

On exit breakpoints

resolve(value)go()lbboSymgeMessadetho

M

saM
es

M

es

sa

ge

ge

shoppingSession<-go()@FutureMessage

REME-D Stepping

40

Step Over
StepInto
IntoStep
Step Return
Step Until

inventory

partInStock
buyerP

credit bureaucheckCredit

goshippercanDeliverPre-experimental User Study
Goal: How real users perceive and value thefeatures of an ambient-oriented (AmOP) debugger.
••One-group pretest-posttest quasi-experiment
design.
22 participants.

41

5GOSHOPPING: DEBUGGING AMBIENTTALK PROGRAMS WITH REME-D

email: egonzale@vub.ac.be
office: 10F731

5goShopping: Debugging AmbientTalk programs withREME-D

Lab session material available at Pointcarre under LabSessions, and at http://soft.
vub.ac.be/˜egonzale under Teaching.

5.1

Idea

The purpose of this exercise is to get familiar with REME-D 1 , a distributed debugger
designed for AmbientTalk applications. To this end, the lab material provides you with
an application that contains errors. You should try to fix them by launching it in theEclipse AmbientTalk plugin in debug mode and using REME-D’s features.

5.2

Finding bugs in the goShopping application

The provided application is a sample shopping application that needs to process purchase orders. Before the shop can acknowledge the order, it must verify three things:
1) whether the requested items are still in stock, 2) whether the customer has provided
valid payment information and 3) whether a shipper is available to ship the order intime. The following picture depicts this application which consists of 4 actors.
product Actor

buyer Actor

partInStockaccount Actor
checkCreditteller

canDeliver

shipper Actor

1 read as remedy1Pre-experimental User Study: Take Home Message•Users value REME-D as tool to make AmOP
programming in AmbientTalk easier.

42Value as a tool to nd bugs
18"
16"
14"
12"

•

REME-D supports expected features for anambient-oriented debugger.

10"
8"
6"
4"
2"
0"

Impact of UI and visualisations.

("0"+"++"

Value as a tool to ease distributed
programming in AmbientTalk
18"
16"
14"
12"
10"
8"
6"
4"

PretestPosttestfi•(("2"0"(("("0"+"++"

Could we build debugging support that..
•deals with non-determinism inherent to distributed systems?

•can be applied to different concurrency models?

•features advanced visualisations for the event-based nature of distributedsystems?

•

is probe-effect free?

•deals with big amounts of data?

•

can be used in environments with memory and network constraints?

43

IDRA and Spa
Practical Online Debugging of Big Data Processing Applications

Matteo Marra, Guillermo Polito, and Elisa Gonzalez Boix. Practical Online Debugging of Spark-like Applications. In Proceedings of the IEEE
21st International Conference on Software Quality, Reliability and Security (QRS). IEEE, p. 620-631 12 p. 2021.

Big Data Processing
Healthcare

Finance

Big Data

SocialMedia

Environment

Long Running
Due to the high volume of data
they have to analyze

Distributed
They remotely execute on clusters, whichslows down the debugging cycle

Bugs in Big Data Processing Applications
46

Code Defect37% of Reported Errors
In cloud Big Data processingservices are attributed to developererrors [Zhou et al. 2015]

Explicit errors inserted by developers

Operation Fault
Common operational mistakes, e.g., file renaming

MisuseA configuration error, e.g., using a wrong library version

Could we build a debugger so that..
Online Debugging
Debug the system when the bug happens

47

Avoid Replays

Global View
Centralised debugging of the distributed system
Domain-Speci c Debugging

Isolation
Debug the system without interfering with its execution

Updates of the Running Systemfifi

Deploy code- xes without restarting the whole distributed system

Live Code Updating

Avoid Replays

Out-of-Place Debugging

Domain-Speci c Debugging
48

WorkerDebug Session
Exception

MasterDebug Session
Exception

WorkerfiDeveloper Machine

ClusterDebugging Events

Avoid Replays
49

Remove Framework Frames

Debugging Session

Captures the execution state throughthe call-stack
Heap

Call-Stack<<local variable>>:TweetOutOfMemoryException >> signal
...
...
...

:TweeterStream

TwitterApplication >> analyzeTweets:TwitterApplication

Reduce the amount of data to be transferred

Include the event-inducing record

I.e., the record that was being processed when thedebugging event (breakpoint or error) happened.

...
<<receiver>>Main >> main

Include the partition of the eventinducing record

The partition of data that was being processed when
the debugging event happened, that includes theevent-inducing record

Distributed Live Code Updates

Live Code Updating
50

WorkerException

PatchCommit

PatchMaster
WorkerDeveloper Machine

ClusterIDRAMR: A Live Debugger for Map/Reduce

Domain-Speci c Debugging

fi51

Debug Single Record

Debug on Virtual Partitions

Select which debugging event todebug starting from the eventinducing record, including its partitionIncluding all of the event-inducing
records, or a merge of all theirpartitions

Spa: a Live Debugger for Spark

Domain-Speci c Debugging
52

Classic stepping operations
Typical of online debuggers

Dedicated stepping operations
Tailored to Spark-like computationsfi

https://www.youtube.com/watch?v=GpipdhVxYq0

Event-based Out-of-place Debugging
Practical Online Debugging of Internet of Things applications

Tom Lauwaerts, Carlos Rojas Castillo, Robert Gurdeep Singh, Matteo Marra, Christophe Scholliers, and Elisa Gonzalez Boix, In,
Proceedings of the 19th International Conference on Managed Programming Languages and Runtimes (MPLR) Association for Computing
Machinery (ACM), p. 85-97 13 p. 2022.

Out of Place Debugging for Internet of Things
54

fi

Non-transferable resources

Domain-Speci c Debugging

55

fi

Non-transferable resources

Domain-Speci c Debugging

56

In Conclusion•

Distributed systems are varied, successful and widespread.

•

They are still challenging to design and implement.

•It is essential to explore novel programming abstractions in tandem with
software tools tailored to modern concurrent and distributed software.

57

Thanks to DisCo & collaborators!
Dominik Aumayr

Aäron Munsters

Jim Bauwens

Florian Myter

Clément Béra

Isaac Nyabisa Oteyo

Dina Borrego

Guillermo Polito

Kevin De Porre

Nuno Preguiça

Carla Ferreira

Carlos Rojas Castillo

Robert Gurdeep Singh

Christophe Scholliers

Tom Lauwaerts

Angel Luis Scull Pupo

Stefan Marr

Carmen Torres Lopez

Matteo Marra…

58

Hanspeter Mössenböck

egonzale@vub.be@elisagboix

https://soft.vub.ac.be/disco/