Information Technology Reference
In-Depth Information
Ta b l e 3 . Use case protocols implemented in Scribble
Global Scribble FSM Memory Generation Time
Use Cases from research papers
(LOC)
(B)
(s)
A vehicle subsystem protocol [21]
8
840
0.006
Map web-service protocol [15]
10
1040
0.010
A bidding protocol [24]
26
1544
0.020
Amazon search service [16]
12
1088
0.010
SQL service [32]
8
1936
0.009
Online shopping system [14]
10
1024
0.008
Travel booking system [14]
16
1440
0.013
Use Cases from OOI and Savara
A purchasing protocol [20]
11
1088
0.010
A banking example [29]
16
1564
0.013
Negotiation protocol [29]
20
1320
0.014
RPC with timeout [29]
11
1016
0.013
Resource Access Control [29]
21
1854
0.018
these factors for each of the listed protocols. The time required for FSM generation
remains under 20 ms, measuring on average to be around 10 ms. The memory overhead
also remains within reasonable boundaries (under 1.5 KB), indicating that FSM caching
is a feasible optimisation approach. The full Scribble protocols can be found at [35].
From our experience of running our conversation monitoring framework within the
OOI system, we expect that, in many large distributed systems, the cost of a decen-
tralised monitoring infrastructure would be largely overshadowed by the raw cost of
communication (latency, routing) and other services running at the same time. Consid-
ering the presented results, we thus believe the important benefits in terms of safety
and management of high-level applications come at a reasonable cost and would be a
realistic mechanism in many distributed systems.
5
Interruptible Session Type Theory and Related Work
5.1
Session Type Theory for Interrupts
In this subsection, we sketch the underlying session type theory with interrupts and
its correctness result, session fidelity , justifying our design choices. We build over the
multiparty session theory [17], adding syntax and semantics for interrupts. In our theory,
global types correspond to session specifications whereas local types are used to express
monitored behaviours of processes [7]. We show that interruptible blocks can be treated
through the use of scopes , a new formal construct that realises, through an explicit
identifier, the domain of interrupts. Our scope-based session types can handle nested
interrupts and multiparty continuations to interruptible blocks, allowing us to model
truly asynchronous exceptions implemented in this paper (these features have not been
modelled in existing MPST theories for exceptions [11,10,9]). The full definitions and
proofs are available from [35].
Search WWH ::




Custom Search