Transcript Component?

Programming and Verifying Distributed and
Adaptable Autonomous Components
with GCM/ProActive
Ludovic Henrio
SCALE Team
INRIA – UNS – I3S – CNRS
Sophia Antipolis
SCALE :
Safe Composition of Autonomous applications
with Large-scale Execution environment
Membrane
m1:
Content
Unified Programming Model
Server Interface
•Multi-level parallelism (multi-active objects)
with rich synchronisation primitives
•Formal methods: spec & verif
•Target Multicore, GPU, Clusters, Clouds, …
Binding
Multicast
Client In
m0: Ty3 −> Ty4
Runtime Support
Application Domains
•
•
•
•
• Big Data
programming analytics
• Simulation
Middleware + VM placement
SLA-aware management
Green scheduling
Debugging and
fault-tolerance
m2:
Primitive Component
m4:
How we use formal methods
Programming
model and
definitions
Generic
properties
Implementation
Java
Optimizations
Verification tools
Model
checking
Optimizations
Agenda
I. Distributed Components: GCM/ProActive
II. Non-functional and autonomic components
III. Dynamic adaptation
IV. Behavioural specification and verification
Why software components?
• Piece of code (+data) encapsulated with well defined
interface
• Very interesting for reasoning on programs (and for
formal methods) because:
 components encapsulate isolated code
 compositional approach (verification, …)
 interaction (only) through interfaces
 well identified interaction  easy/safe composition
Reasoning and programming is easier and compositional
 Potential for compositional verification
What are Components?
Primitive component
Business code
Server
/ input
Client
/ output
What are Components?
Composite component
Primitive component
Business code
Primitive component
Business code
 Grid Component Model (GCM)
An extension of Fractal for Distributed computing
But what is a Good size for a
(primitive) Component?
Not a strict requirement, but somehow imposed by the
model design
• According to CCA or SCA, a service (a component
contains a provided business function)
• According to Fractal, a few objects
• According to GCM, a process
 In GCM/ProActive,
1 Component (data/code unit)
= 1 Active object (1 thread = unit of concurrency)
= 1 Location (unit of distribution)
GCM: A Grid Extension to Fractal for Autonomous Distributed Components - F. Baude, D.
Caromel, C. Dalmasso, M. Danelutto, V. Getov, L. Henrio, C. Pérez - Annals of Telecom. - 2008
A Primitive GCM Component
CI
CI.foo(p)
 Primitive components communicate by asynchronous
requests on interfaces
 Components abstract away distribution and concurrency
 In ProActive/GCM a primitive component is an active
object
Futures for Components
1
f=CI.foo(p)
……….
g=f+3
2
3
Component are independent entities
(threads are isolated in a component)
+
Asynchronous requests with results

Futures are necessary
First-class Futures
f=CI.foo(p)
CI.foo(f)
…
…
…
Only strict operations are blocking (access to a future)
Communicating a future is not a strict operation
First-class Futures and Hierarchy
return C1.foo(x)
… …
…
Without first-class futures, one thread is systematically
blocked in the composite component.
A lot of blocked threads
In GCM/ProActive  systematic deadlock
Collective interfaces (GCM)
• One-to-many = multicast
• Many-to-one = gathercast
• Distribution and synchronisation/collection policies for
invocation and results
Composite component
Primitive component
Business code
Primitive component
Business code
Primitive component
Business code
Primitive component
Business code
Multi-Active GCM/ProActive Component
Provided add, add and monitor are compatible
add() {
CI.foo(p)
}
add() {
…
…}
monitor()
{…
…}
Note: monitor is compatible with join
Compatibility annotations
Groups
(Collection of related
methods)
Rules
(Compatibility relationships
between groups)
Memberships
(To which group each
method belongs)
A new programming model
• Multi-active objects feature:
 Active object model



Local concurrency and efficiency on multi-cores



Easy to program
Support for distribution
Transparent multi-threading
Safe parallel execution
Possibility to write non-blocking re-entrant code
 Simple annotations
Summary:
A Distributed Component Model with Futures
•
•
Primitive components contain the business code
Primitive components act as the unit of distribution
and concurrency
each thread is isolated in a component
•
•
Communication is performed on interfaces and follows
component bindings
Futures allow communication to be asynchronous
requests in a transparent way
Programming distributed and adaptable autonomous components—the GCM/ProActive
framework. F. Baude, L. Henrio, and C. Ruz Software: Practice and Experience – 2014
A Framework for Reasoning on Components
• Formalise GCM in a theorem prover (Isabelle/HOL )
Component hierarchical Structure
Composite component
Primitive component
• Bindings, etc…
• Design Choices
 Suitable abstraction level
 Suitable representation (List / Finite Set, etc …)
• Basic lemmas on component structure
Business code
Primitive component
Business code
Prove Generic
properties
A Framework for Reasoning on Component Composition
Ludovic Henrio, Florian Kammüller, and Muhammad Uzair Khan - FMCO 2009, Springer
Agenda
I. Distributed Components: GCM/ProActive
II. Non-functional and autonomic components
III. Dynamic adaptation
IV. Behavioural specification and verification
Separation of concerns in GCM architecture
• Content: responsible
for business logic
• Membrane: responsible
for control part
• Functional and nonfunctional interfaces
• Business logic and
control part can be
designed separately
Autonomic components:
MAPE loop in GCM/ProActive
Actions
Rules
Interface Interface
Monitoring
Interface
A
metrics
Monitoring
Analysis
alarm
Planning
Execution
actions
C
B
(b)
Actions Monitoring
Interface Interface
Interceptor components
• Example: Monitoring and reconfiguration
 Component architecture becomes complex
 Need a procedure to decide its correctness
How do we recognize interceptors chains?
• all the components are nested
inside the membrane
• all the components have
exactly one functional server
and one functional client
interface
• The interceptors form a chain
• the first and the last
components of the chain are
connected to the composing
component
Static properties and validation rules (1)
Component
encapsulation
Bindings do not cross the
boundaries of the
components
Correct typing
Interfaces connected by
bindings have compatible roles
Interfaces connected by
bindings have compatible
methods
Static properties and validation rules (2)
Deterministic
communications
Each client interface is
connected to at most
one server interface
(except multicast)
Unique naming
Interfaces have unique
names inside a container
Components have unique
names inside a container
Static properties and validation rules (3)
Separation of
concerns
The interfaces connected by a binding should
have compatible control levels
• CL of a functional interface = 1
• CL of a non-functional interface = 2
• CL is increased by 1 for interfaces of controllers
• Compatible CLs: either both = 1, or both >1
Static properties and validation rules (4)
• CL of a functional
interface = 1
12
• CL of a nonfunctional interface
=2
2
2
• CL is increased by
1 for interfaces of
controllers
• Compatible CL:
either = 1, or >1
1
2
1
1
1
1
2
A formal model for GCM architecture
• Define and formalize
well-formed components
 Usual fractal structure
 Non-functional
components
 Interceptors
Architecture
Compos = CName <SItfi iÎI ,CItf j jÎJ , Membr, Cont>
Membr =< CompllÎL , BindingnnÎN >
Cont =< SItfi iÎI , CItf j jÎJ , CompllÎL , BindingnnÎN >
SItf = (Name, MSignature, Nature)S
Wellformness
• A graphical specification
environment for GCM
components modeling
and static validation
WF(< SItfi iÎI , CItf j jÎJ , CompllÎL , BindingnnÎN >) Û
ìUniqueItfNames(SItfi iÎI ÈCItf j jÎJ )Ù
ï
ïUniqueCompNames(CompllÎL )Ù
ï
íCardValidity(BindingnnÎN )Ù "k Î K.WF(Compk )Ù
ï
nÎN
ï"B Î Bindingn .BindingRoles(B)Ù
ï BindingTypes(B)Ù BindingNature(B)
î
Verifying the correct composition of distributed components: Formalisation and Tool
Ludovic Henrio, Oleksandra Kulankhina, Dongqian Liu, and Eric Madelaine. FOCLASA 2014
30
Tool: VerCors
• Based on Obeo
Designer
• Graphical
environment for
GCM
Components
and UML
Diagrams
Produces ADL files, Java classes and Java interfaces
Distributed as Eclipse plugins
Agenda
I. Distributed Components: GCM/ProActive
II. Non-functional and autonomic components
III. Dynamic adaptation
IV. Behavioural specification and verification
Adaptation in the GCM
• Functional adaptation: adapt the architecture
+ behaviour of the application to new
requirements/objectives/environment
• Non-functional adaptation:
adapt the architecture of the container+middleware to
changing environment/NF requirements (QoS …)
• Both functional and non-functional
adaptation are expressed as
reconfigurations
A Component Platform for Experimenting with Autonomic Composition
Françoise Baude, Ludovic Henrio, and Paul Naoumenko. Autonomics 2007.
Triggering Distributed Reconfigurations in the
Scripting Language: GCMScript
• Fscript is a language to reconfigure Fractal components
• A primitive for the distributed script interpretation
remote_call(target_component, action_name, parameters, ...);
• + other minor extensions
Reconfiguration interface
target_component
Interpreter
action(arguments)
Example
RC 2
definition action1
Reconfiguration
interface
...
remote_call(C2,’action2’)
remote_call(C11,’action11’)
remote_call(C12,’action12’)
Reconfiguration scripts
C2
...
definition action12
...
RC 1
remote_call(C121,’action121’)
...
Interpreter
RC 11
Membrane
RC 12
C11
RC 121
Example
RC 2
definition action1
Reconfiguration
interface
...
remote_call(C2,’action2’)
remote_call(C11,’action11’)
remote_call(C12,’action12’)
Reconfiguration scripts
C2
...
action1( )
definition action12
...
RC 1
remote_call(C121,’action121’)
...
Interpreter
RC 11
Membrane
RC 12
C11
RC 121
C121
C12
Example
RC 2
definition action1
Reconfiguration
interface
...
remote_call(C2,’action2’)
remote_call(C11,’action11’)
remote_call(C12,’action12’)
Reconfiguration scripts
C2
...
action1( )
action2( )
definition action12
...
RC 1
remote_call(C121,’action121’)
...
Interpreter
action11( )
Membrane
action12( )
11
The reconfiguration script is RC
executed
inRC
a 12
parallel and
distributed manner
C11
RC 121
 GCM-script language
C121
C12
C1
A Reconfiguration Framework for Distributed Components
Marcela Rivera, Ludovic Henrio and Boutheina Bannour. SINTER Workshop 2009
Typical usecase – Farm pattern
R1: {avgReqServPerSec,<,tL}
R2: {avgIdleCPU,>,tI}
F
avgReqServPerSec
avgIdleCPU
totalFreeDisk
totalFreeMem
Mf
Af
Ef
Pf
freeRepositorySpace
caller
W1
Mr
workers
front-end
repo
G
W2
repo
R
repo
master
master
reqServPerSec
idleCPU
freeDisk
freeMem
W3
Agenda
I. Distributed Components: GCM/ProActive
II. Non-functional and autonomic components
III. Dynamic adaptation
IV. Behavioural specification and verification
Motivating example: What Can Create
Deadlocks in ProActive/GCM?
• A race condition:
• Detecting deadlocks can be difficult  behavioural specification and
verification techniques
How to ensure the
correct behaviour of a given program?
• Theorem proving too complicated for the ProActive
programmer
• Our approach: behavioural specification
Service methods
Service methods
Step to be fully
automatized
pNets:
 Trust
the implementation step
 Or static analysis
 Generate correct (skeletons of) components from
Vercors specification (+static and/or runtime checks)
Behavioural Models for Distributed Fractal Components Antonio Cansado, Ludovic
Henrio, and Eric Madelaine - Annals of Telecommunications - 2008
Use-case: Fault-tolerant storage
•
1 multicast interface sending write/read/commit requests
to all slaves.
• the slaves reply asynchronously, the master only needs
enough coherent answers to terminate
Verifying Safety of Fault-Tolerant Distributed Components
Rabéa Ameur-Boulifa, Raluca Halalai, Ludovic Henrio, and Eric Madelaine - FACS 2011
Full picture: a pNet
Support for parameterised
families
?Q_Write(x)
!Q_Write(b)
Synchronisation vectors
Basic pNets: parameterized LTS
Labelled
transition
systems, with:
•Value passing
•Local variables
•Guards….
Can be written
as a UML
diagram
Eric MADELAINE
Properties proved
• Reachability:
1- The Read service can terminate
fid:nat among {0...2}. ∃ b:bool. <true* . {!R_Read !fid !b}> true
2- Is the BFT hypothesis respected by the model ?
< true* . 'Error (NotBFT)'> true
• Inevitability:
After receiving a Q_Write(f,x) request, it is (fairly) inevitable that the Write
services terminates with a R_Write(f) answer, or an Error is raised.
• Functional correctness:
After receiving a ?Q_Write(f1,x), and before the next ?Q_Write, a
?Q_Read requests raises a !R_Read(y) response, with y=x
Prove
generic properties
like absence
of(MCL),
deadlock
(written in
mu-calculus
or Model Checking
Language
Mateescu et al,
FM’08) or properties specific to the application logic
Conclusion
Each component has its
own state and its own
activity (threads)
• Asynchronous and ``autonomous’’ distributed components
 Based on (Multi-)Active object and futures
 Communicate by asynchronous requests and replies
Adapted to large-scale distribution
• Convenient for programming autonomic computing and
adaptation procedures
 Programming model and decoupling of entities
 Componentized membranes and monitoring components
 Specified architecture correctness
• Convenient for verifying correct execution of distributed
applications
 Behavioural specification and model-checking
Implemented: GCM/ProActive
+ a specification and development environment: Vercors
Current and Future works
• Multi-active objects: a new and powerful programming
language
very convenient for programming components
• Verifying reconfiguration procedures
 First results in model-checking
 First specification and generic results in Isabell/HOL
Next steps:
Mixing the two approaches?
Parameterized architecture
• Application to Image recognition algorithms (with C Ruz)
 Autonomic adaptation
 Large data sets
THANK YOU  ----- Key recent publications
•
•
•
•
•
•
Programming distributed and adaptable autonomous components—the
GCM/ProActive framework Françoise Baude, Ludovic Henrio, and Cristian
Ruz - Software: Practice and Experience 2014
Verifying the correct composition of distributed components:
Formalisation and Tool. Ludovic Henrio, Oleksandra Kulankhina, Dongqian
Liu, and Eric Madelaine. FOCLASA 2014
Multi-threaded Active Objects. Ludovic Henrio, Fabrice Huet, and Zsolt
István - In COORDINATION 2013, Springer. 2013.
Formally Reasoning on a Reconfigurable Component-Based System - A
Case Study for the Industrial World. Nuno Gaspar, Ludovic Henrio, Eric
Madelaine - In FACS'2013.
A Framework for Reasoning on Component Composition
Ludovic Henrio, Florian Kammüller, and Muhammad Uzair Khan - FMCO 2009
GCM: A Grid Extension to Fractal for Autonomous Distributed
Components. F. Baude, D. Caromel, C. Dalmasso, M. Danelutto, V. Getov, L.
Henrio and C. Pérez. Annals of Telecommunications - Special Issue on
Software Components - The Fractal Initiative, Springer, 2009