CS 735: Formal Models for Concurrent and Asynchronous Systems

(1)

CS 735: Formal Models for Concurrent and Asynchronous Systems

–Introduction

Instructor: Akshay S.

Jul 30, 2019

Course hours: Slot14, Tuesdays and Fridays 5:30-7:00pm

Office hours: To be announced

1

(2)

CS 735: Formal Models for Concurrent and Asynchronous Systems

–Introduction

& and Prof. Krishna (for one module) Jul 30, 2019

(3)

CS 735: Formal Models for Concurrent and Asynchronous Systems

–Introduction

& and Prof. Krishna (for one module) Jul 30, 2019

Queries: Email me with [CS735-2019] in subject line akshayss@cse.iitb.ac.in

1

(4)

Goal

Formal Models for distributed and infinite-statesystems

I Distributed: Concurrent, asynchronous, communicating,...

I Formal models: Mathematical description, graphical notations, Automata models

(5)

Goal

Formal Models for distributed and infinite-statesystems I Distributed: Concurrent, asynchronous, communicating,...

2

(6)

Goal

GROUND _OPS entry : GROUND _OPS _ACTIVE = TRUE ; evaluate _ conditions ();

during : evaluate _ conditions ();

5.2 (1)

GROUND _MODE _SELECTION 5.2.1

AUTOMATIC _REFUEL MANUAL _REFUEL

5.2. 2 5. 2. 3 DEFUEL

5.2. 4

AR _CONFIRM / AR _AUTO_SOT = FALSE ; MR_CONFIRM /

DF_CONFIRM

GT_CONFIRM /

OFF_CONFIRM

SHUT _OFF _TEST GROUND _TRANSFER

5. 2.5 OFF

5.2.6 5. 2.7 function

evaluate _conditions 5.2 (2)

function

GO _ D = DELAY ( d _ t) [( MANUAL_REFUEL | ...

GROUND _SEL _FAULT) & ...

DELAY (DELAY _MODE _SEL )]

1

[(( IRP_AUTO _REFUEL & ...

~ GROUND _SEL _FAULT) | ...

(ICP _AUTO_REFUEL)) & ...

DELAY (DELAY _MODE _SEL)]

1

[(ICP _AUTO _REFUEL & ...

AR_AUTO_SOT ) | ...

(IRP _AUTO_REFUEL & ...

AR_AUTO_SOT )]

2

[(ICP _AUTO_REFUEL & ...

~ AR_AUTO_SOT ) | ...

(IRP_AUTO _REFUEL & ...

~ AR_AUTO_SOT ) ]

1

[( ~IRP _AUTO _REFUEL & ...

~ ICP _AUTO_REFUEL) | ...

GROUND _SEL _FAULT]

2

[ ~MANUAL_REFUEL & ...

~ GROUND _SEL _FAULT]

[(IRP _AUTO_REFUEL & ...

~ GROUND _SEL _FAULT) | ...

(ICP_AUTO _REFUEL)] / d_i=0;

1

[(DEFUEL _MODE & ...

~ GROUND _SEL_FAULT) & ...

DELAY (DELAY_MODE _SEL )]

1

[ ~ DEFUEL _MODE | ...

GROUND _SEL _FAULT] [ ~MANUAL_REFUEL & ...~ GROUND _SEL _FAULT]

2

[( ~IRP _AUTO_REFUEL & ...

~ ICP _AUTO_REFUEL ) | ...

GROUND _SEL _FAULT]

2

[MANUAL_REFUEL | ...

GROUND_SEL _FAULT] / d_i=0;

6

[DEFUEL _MODE & ...

~ GROUND _SEL _FAULT] / d_i=0;

5

[ ~DEFUEL_MODE | ...

GROUND _SEL _FAULT]

2

[(SOT _INITIATED & ...

~ GROUND _SEL _FAULT)] ...

{AR_AUTO_SOT = FALSE;}

2

[GROUND _TRANSFER & ...

~GROUND _SEL _FAULT] / d_i= 0;

4

[ ~GROUND _TRANSFER | ...

GROUND _SEL _FAULT]

1

[System _State[ SS_SOT _COMPLETE ] &... .

~ ICP _AUTO_REFUEL & ~ IRP _AUTO_REFUEL]

1

[ ~GROUND _TRANSFER | ...

GROUND _SEL _FAULT]

[OFF _MODE _SEL & ...

~ GROUND _SEL _FAULT] / d_i=0;

3

[~OFF _MODE _SEL | ...

GROUND _SEL _FAULT]1

[ ~OFF _MODE _SEL | GROUND _SEL _FAULT]

[(GROUND _TRANSFER & ...

~ GROUND_SEL _FAULT) & ...

2

[( OFF_MODE _SEL & ...

~ GROUND _SEL _FAULT) & ...

2

(7)

Goal

I Infinite-state: variables over an infinite domain: counters, channel/queue size, data, time, probabilities

2

(8)

Goal

I Infinite-state: variables over an infinite domain: counters, channel/queue size, data, time, probabilities

Questions that we will tackle I Analysis of such models I Characterization, relations

I Underlying properties, generalizations

(9)

Course contents

Topics and models that we will cover in this course:

1. Petri nets

2. Well-structured transition systems

3. Distributed automata models and their behaviors 4. Applications to concurrent programs

3

(10)

Course contents

1. Petri nets

I Elementary nets, Place/Transition nets I Behaviors - traces, posets, unfoldings.

I Decision problems - reachability, coverability I Tools, implementations and case-studies (optional) 2. Well-structured transition systems

3. Distributed automata models and their behaviors 4. Applications to concurrent programs

(11)

Course contents

1. Petri nets

I A generalized abstraction for infinite-state systems I Well-quasi orders and well-founded systems

I Applications to show termination of infinite systems I Theoretical bounds on complexity (optional) 3. Distributed automata models and their behaviors 4. Applications to concurrent programs

3

(12)

Course contents

1. Petri nets

I Applications to show termination of infinite systems I Theoretical bounds on complexity (optional) 3. Distributed automata models and their behaviors

I Asynchronous automata

I Message passing automata and Lossy channel machines 4. Applications to concurrent programs

(13)

Course contents

1. Petri nets

I Applications to show termination of infinite systems I Theoretical bounds on complexity (optional) 3. Distributed automata models and their behaviors

I Asynchronous automata

I Message passing automata and Lossy channel machines 4. Applications to concurrent programs

I Modeling “weak” memory in programs: variants, algorithms I Towards efficiency: (Dynamic) partial order reductions

3

(14)

Automata

a c b

a

a b c a b

I Behaviours are words, i.e., sequences of actions over a finite alphabet Σ ={a,b,c}.

Questions

I How shall we distribute it?

I How shall we add concurrent behaviors?

(15)

Automata

a c b

a

a b c a b

Questions

4

(16)

Petri Nets

• •

•

I An old model for distributed systems

I invented by Carl Petri (-at the age of 13- in 1939? or ’62) I to model resource consumption and so on...

(17)

Examples of Petri nets

I A chemical reaction: 2H2+O2 →2H2O.

I A library

I A producer-consumer example I A coffee machine

6

(18)

Examples of Petri nets

I A library

(19)

Examples of Petri nets

I A library

Applications: Business process models, stochastic processes, biological networks and so on

6

(20)

Automata

a c b

a

a b c a b

Questions

(21)

Automata

a c b

a

a b c a b

Questions

7

(22)

Asynchronous Automata

a c b

a

a b c a b

(23)

Asynchronous Automata

c

a b

p a

c a

q

b c b

I Actions are distributed across processes (with sharing!) I Some actions are shared, e.g., cis allowed only if both p

and q move onc.

8

(24)

Asynchronous Automata

c

a b

p a

c a

q

b c b

I What are the properties of languages accepted by such automata? E.g. above accepts {abcab, bacab, bacba, abcba}.

I Given a languageL, (when) can it be accepted by such an asynchronous automaton?

(25)

Message Passing Automata

c→

a b

p a

a

q

b

b c

I In fact, this formalism is Turing powerful!

I We will consider decidability issues.

I (Surprising fact: If you are allowed to lose messages randomly then it is decidable!) These are called Lossy channel systems.

9

(26)

Message Passing Automata

c→

a b

p a

a

q

b

b c

I (Surprising fact: If you are allowed to lose messages randomly then it is decidable!)

These are called Lossy channel systems.

(27)

Message Passing Automata

c→

a b

p a

a

q

b

b c

I (Surprising fact: If you are allowed to lose messages randomly then it is decidable!) These are called Lossy channel systems.

9

(28)

Applications to Concurrent programs

What are good formal models for concurrent programs?

I Automata or transition systems

I Distributed/Asynchronous/Message-passing automata?? I Petri nets

Does this capture reality of programs in today’s world?

(29)

Applications to Concurrent programs

I Distributed/Asynchronous/Message-passing automata??

I Petri nets

10

(30)

Applications to Concurrent programs

I Distributed/Asynchronous/Message-passing automata??

I Petri nets

(31)

Modeling concurrent programs

Two issues

I In the multi-processor world: memory access is no longer atomic!

I There is no non-determinism! How to avoid exploring runs Leads to:

1. Weak memory models

2. Partial order reduction techniques

11

(32)

Modeling concurrent programs

Two issues

I In the multi-processor world: memory access is no longer atomic!

I There is no non-determinism! How to avoid exploring runs Leads to:

1. Weak memory models

2. Partial order reduction techniques

(33)

Generalizing...

I In general, these are examples of infinite-state objects.

I If you don’t like “state objects”, think of them as infinite discrete structures!

I Why?

Another title for this course:

Reasoning about infinite (discrete) structures! I Theory of well-structured transition systems I Under-approximate verification

I Fixed-point approaches

Pictures and Mathematics

I How do you write these objects mathematically? I Why write them mathematically?

12

(34)

Generalizing...

I Why?

(35)

Generalizing...

I Why?

12

(36)

Generalizing...

I Why?

Reasoning about infinite (discrete) structures!

I Theory of well-structured transition systems I Under-approximate verification

(37)

Generalizing...

I Why?

12

(38)

Generalizing...

I Why?

I How do you write these objects mathematically?

I Why write them mathematically?

(39)

Some take-aways from this course

I Different formal models for distributed systems

I Mathematical formalisms that reason about (the infinite) behaviors of such systems.

I Techniques to automatically analyze such systems.

I How to use them and where they are applied.

13

(40)

Logistics

Evaluation (flexible... upto a point)

I Continuous evaluation - assignments/quizzes : 40%

I Exam (Midsem/Endsem): 35 % I Paper presentation: 25 %

There will be guest lectures, research directions given along the way.

Course material, references will be posted at

I http://www.cse.iitb.ac.in/~akshayss/teaching.html I Piazza will be set up soon?

(41)

Logistics

Evaluation (flexible... upto a point)

I Continuous evaluation - assignments/quizzes : 40%

I Exam (Midsem/Endsem): 35 % I Paper presentation: 25 %

There will be guest lectures, research directions given along the way.

Course material, references will be posted at

I http://www.cse.iitb.ac.in/~akshayss/teaching.html I Piazza will be set up soon?

14