Aplicações:
Leitores – Escritores
Um Piloto Automático (Cruise Control)
Alexandre Sztajnberg
1o Workshop do Projeto VAS
PDPG-TI CNPq 552192/02-3
Março / 2004
IC/UFF, Niterói
Escritores e Leitores
• Objetivos
– Modelar através de contratos de coordenação
• Concorrência e exclusão mútua
• Sincronização
• Prioridades no nível da aplicação
– starvation
– Verificação formal
Escritores e Leitores
• The following requirements should be attended:
– The access among readers can be concurrent
– The access of a writer has to be exclusive considering other writers
and all readers
– If a writer is writing, the priority is for readers (if any waiting to
read)
– If there are readers reading, and a writer arrives, the priority is for
the writer. In that case, if new readers come, they cannot begin to
read before the waiting writer writes
• Problems to solve:
– Application level priority without explicit alternate between
readers and writers, avoiding starvation
– Relax concurrency to readers, while imposing exclusivity to
writers and maintaining consistency
Conector em CBabel (i)
red connector 'READ_WRITE {
int
boolean
int
int
int
'Readers, 'Writers ;
'Writing ;
'Want-to-read, 'Want-to-write;
'turn;
R = 0, W = 1;
// readers actually reading
// a writer is writing
// number of potential
in port 'can-I-read ;
in port 'can-I-write ;
out port 'ok-to-read ;
out port 'ok-to-write ;
selfexclusive {'can-I-write ; } // *** ver se o efeito produzido é o desejado !!!
} 'RW .
Conector em CBabel (ii)
interaction {
'can-I-read > guard (true) {
before {'Want-to-read = 'Want-to-read + 1} }
>
guard (('Writing == false) AND
((´Want-to-Write == 0) OR ('turn == R))) {
before {'Want-to-read = 'Want-to-read - 1;
'Readers = Readers + 1;
if ('Want-to-read == 0) 'turn = W;} // or simply 'turn = W
after {'Readers = 'Readers - 1;} }
> 'ok-to-read ;
'can-I-write > guard (true) {
before {'Want-to-write = 'Want-to-write + 1} }
>
guard ((('Readers == 0) AND (´Writing == false)) AND
(('Want-to-read == 0) OR ('turn == W))) {
before {'Want-to-write = 'Want-to-write - 1;
'Writing = true; 'Writers = Writers + 1; }
after {'Writing = false; 'Writers = Writers - 1;
'turn = R; } }
> 'ok-to-read ;
}
Observation
• The expected result of the “exclusive {'can-I-write ; }” statement is to
enforce mutual exclusion among Writers and allow concurrency
among Readers. Nevertheless, the overall mutual exclusion property
for the application is reinforced with the guards.
• Besides we are considering that, even though the reader interaction
path in the connector (‘can-I-write > guard > guard > ‘ok-to-read) is
not tagged as exclusive (or self exclusive)
– the first part of the guard construction (i.e, verifying the condition holds,
taking the message, evaluating the before clause) is atomic.
– In this way even before a reader stops reading (the return, the after clause
evaluation and the return propagation) an other reader can start to read.
Verificações
a) Escritores acessam o recurso compartilhado em exclusão mútua com Leitores e outros
Escritores. Se existe um Escritor escrevendo, então não existem Leitores lendo e apenas
um Escritor escrevendo.
(Writing = TRUE)  ((Readers = 0)  (Writers = 1))
(a)
b) Se existe algum leitor ativo e não existem escritores suspensos aguardando oportunidade
para escrever, então não existe motivo para outros leitores estarem esperando para ler, já
que leitores não precisam de exclusão mútua entre si.
((Readers > 0)  (Want-to-write = 0) or (turn = R)  (Want-to-read = 0)
(b)
c) Se existe um escritor ativo e temos leitores e escritores suspensos nos respectivos guardas,
aguardando permissão para agir, então a prioridade será dada aos leitores, que só poderão
agir quando o escritor terminar.
((Writing = TRUE)  (Want-to-readr > 0)  (Want-to-write > 0)) 
(( (Writing = FALSE))  (( Want-to-read = 0) until (Writing = FALSE)))
(c)
d) Podemos capturar, ainda, grande parte das propriedades desejadas no problema na seguinte
fórmula. Se existem leitores em atividade e escritores e leitores suspensos. Isso significa
que os leitores suspensos chegaram em uma hora em que já haviam escritores suspensos.
Então os leitores somente terão oportunidade de ler depois que um escritor suspenso
conseguir escrever.
((Readers > 0)  (Want-to-write > 0)  (Want-to-read > 0)) 
(( Want-to-read = 0) until (Writing = TRUE))
(d)
Próximos passos
• Tradução para Maude
– Composição de conectores com contratos
elementares
• Model checking
Cruise Control
• Cruise control
– Baseado no exemplo do livro Concurrency
– Sistema de interlocking  Interações assíncronas
• Podem ser modeladas por guardas de CBabel ?
• Separação dos módulos funcionais / sistema de interlocking
• Modelo de execução (CBabel) x modelo abstrato baseado em LTS (livro)
– Modelo abstrato facilita a verificação
• Precisa de um passo para mapear o modelo em uma implementação
– Modelo em CBabel + tradução para Maude
• Já pressupõe um modelo que pode ser executado
• Verificação através de Maude
Cruise control configuration
carInput
splitter
carController
engineOn
carSimulator
engineOff
engine loop
accelerator
getThrottle
setThrottle
getSpeed
breack
cruiseController
enableControl
disableControl
cruiseInput
recordSpeed
on
clearSpeed
off
correta
resume
tranco
speedController
speedControlPace
sleep 500
setSpeed
Módulo carInput
• Models a standard set of input
controls of a car.
• They can be activated
asynchronously, at any time.
• The human driver dictates the
best use.
carInput
engineOn
engineOff
accelerator
breack
module carInput {
out port oneway
out port oneway
out port oneway
out port oneway
}
()
()
()
()
engineOn;
engineOff;
accelerate;
brake;
Módulo cruiseInput
• This module encapsulates the
controls provided by the cruise
controller device.
• The human driver is free to use
it as he will.
cruiseInput
on
off
resume
module controlInput {
out port oneway (void) on;
out port oneway (void) off;
out port oneway (void) resume;
}
Módulo speedControlPace
•
•
•
The only purpose of this module is
to impose a pace to the
speedController connector when
the cruise control mechanism is
active.
It provides the interval time
between a sampling of the actual
car speed and the respective throttle
correction to maintain the set
speed.
Obs: O objetivo e' ativar a porta de
saída setSpeed de tempos em tempos
durante a atuação do speedControl
module speedControlPace {
out port oneway (void)
setSpeed {
// the
speed controller thread
while (true) {
sleep(500);
}
}
}
speedControlPace
sleep 500
Módulo carSimulator
•
•
•
•
Car engine and sensors that can capture
the actual speed / throttle and brake
pedals.
Accepts break and throttle stimulus to
stop / accelerate the car engine.
The car engine is modeled by the run()
method, which is not attached to an
architectural port (this is hidden from
the architecture).
When this module is instantiated, the
engine begins to work. If the car is
not powered on (engineOn out port
was not stimulated), the car cannot
be accelerated (this is controlled by
the connectors).
module CarSimulator {
// begins execution as soon as the application is
up
public void run() {
while (true) {
sleep (1000/ticksPerSecond);
if (fspeed>maxSpeed) fspeed=maxSpeed;
if (fspeed<0) fspeed=0;
fdist = fdist /ticksPerSecond;
speed = (int)fspeed;
}
}
in port oneway (double t, int b) setThrottle
{
throttle=t; brakepedal=b;
if (throttle < 0.0) throttle=0.0;
if (throttle > 10.0) throttle=10.0; }
in port int (void) getThrottle {
return throttle; }
carSimulator
in port int (void) getbrakepedal {
return brakepedal; }
engine loop
getThrottle
setThrottle
getSpeed
in port int (void) getSpeed {
return speed; }
}
Conector splitter
interaction {
brake-in >
(brake-out1 || brake-out2);
splitter
carInput
carController
accelerator-in >
(accelerator-out1 ||
accelerator-out2);
engineOn
engineOff
accelerator
breack
engineOff-in >
(engineOff-out1 ||
engineOff-out2);
cruiseController
enableControl
disableControl
recordSpeed
clearSpeed
correta
engineOn-in >
(engineOn-out1 ||
engineOn-out2);
}
} // splitter
Conector carController
interaction {
engineOn > guard (ignition == false) {
connector
CarController {
carController
carInput before {ignition
= true;
splitter
in port oneway (void)
brake;
carSimulator
// instantiate
carSimulator eengine
link
engineOn
loopcarSimulator }
in
port
oneway
(void)
accelerator;
engineOff
alternative
(ground);
in
port oneway
(void) engineOff;
accelerator
getThrottle
breack
setThrottle
> ground;
in port oneway (void) engineOn;
getSpeed
out port> oneway
int)==setTrottle;
engineOff
guard (double,
(ignition
true) {
staterequired
double
getThrottle;
before
{ignition
= false;
staterequired int getbreakpedal;
// remove carSimulator }
(ground);
exclusive alternative
{engineOn, engineOff,
accelerate, break}
•> ground;
Controls
ignition
– Engine
? {
accelerate
> instantiation
guard (true)
}
– before
Engine{link ?
if (_brakepedal
= getbrakepedal
• Translates
the carInput stimulos
into engine> 0) _brakepedal=0;
else {if (g_throttle=getThrottle<(maxThrottle-1))_throttle += 1.0;
stimulus
else _throttle = maxThrottle; }}
•
Avois breacing and accelerating at the same time
> setThrottle (_throttle, _breakepedal);
brake > guard (true) {
before {
if (_throttle = getThrottle > 0.0) _throttle=0.0;
else if (_brakepedal=getbrakepedal<maxBrake)_brakepedal +=1; }}
> setThrottle (_throttle, _breackepedal);
}
Conector cruiseController
•
Componente principal da lógica de
interlocking da aplicação
– Máquina de estados verificável no
carInput
livro
connector Controller {
int INACTIVE = 0; int ACTIVE
int CRUISING = 2; int STANDBY
int controlState
= 1;
= 3;
= INACTIVE;
engineOn
engineOff
accelerator
breack
cruiseController
enableControl
out
out
out
out
port
port
port
port
oneway
oneway
oneway
oneway
()
()
()
()
disableControl;
enableControl;
clearSpeed;
recordSpeed;
out port oneway () correta;
disableControl
recordSpeed
clearSpeed
cruiseInput
correta
on
exclusive {brake, accelerator,
engineOff, engineOn, on, off,
resume}
interaction {
brake > guard (controlState==CRUISING) {
alternative (ground);
speedController after {controlState=STANDBY;} }
> disableControl;
off
resume
tranco
setSpeed
accelerator > guard
(controlState==CRUISING) {
alternative (ground);
after {controlState=STANDBY;} }
> disableControl;
} // end Control
Conector speedController
connector
SpeedControl
{
interaction
{
int recordSpeed
DISABLED = 0;> guard (true)
//speed{before
control {setSpeed=getSpeed;}}
states
int ENABLED = 1;
alternative
(ground);
•int Em
cruzeiro,
este
conector
state
= DISABLED;
//initial state
ground;= 0;controla a velocidade
int >efetivamente
setSpeed
//target cruise control speed
clearSpeed()
> guard
{before {setSpeed=0;}}
staterequired
int getSpeed;
// getSpeed special port
do motor, acelerando
e (state==DISABLED)
in
•in
•in
in
alternative
(ground);
desacelerando quando
necessário
port
oneway (void) recordSpeed;
> ground;
uma
malha (void)
de controle
port
oneway
enableControl()
>clearSpeed;
guard (state==DISABLED) {before {state=ENABLED}};
port
oneway
(void)
enableControl;
precisa do speedControlPace
para (ground);
alternative
port oneway (void) enableControl;
ritmo a este controle
>dar
ground;
in port oneway (void) setSpeed;
disableControl()
> guard (state==ENABLED)
cruiseController
{before
{state=DISABLED}};
out port enableControl
oneway (float)
setThrottle;
alternative (ground);
disableControl
> ground;
exclusive
{recordSpeed;
clearSpeed; enableControl; disableControl; setSpeed}
recordSpeed
carSimulator
setSpeed >
speedController
clearSpeed
}
guard (state==ENABLED) {before { engine loop
correta
getThrottle
error = setSpeed - getSpeed
/ 6.0;
setThrottle
getSpeed
steady
= setSpeed / 12.0;
speedControlPace
setSpeed
} }
sleep 500
alternative (ground);
> setThrottle(steady+error); //simplified feed back control
}}
Verificações
Safety properties
• When the car is accelerated and the break pedal is pressed, the car will eventually stop
• When the cruise control is eventually activated by pressing the on or resume controls, then
pressing the off, brake or accelerator control deactivates the cruise control.
Progress properties
• If the throttle is eventually set, the car has to accelerate, if the break pedal is not pressed.
The zooming problem
• The “zooming” problem is detected by checking the progress property (reachability ???)
• The problem is detected in the following sequence:
EngineOn  CruiseOn (recordSpeed  setThrottle)  engineOff  engineOn  ZOOM
–
When the engine was set off, the cruise controller was not disabled. When the engine was turn on
again, the cruise controller starts working and sets the throttle to the last recorded speed (that can be
high).
Solution
• Assure that when the engine is turned off, the cruise control is also disabled (or at least clear
the registered speed).
• In our approach another connector is inserted in the interaction path between the external
controls and the engine to achieve this functionality. This is typically the case of a
reconfiguration on the coordination aspect of the application, which is separate form the basic
functionality concerns.
Destaques
• Interações assíncronas
– Modelam bem os controles de um carro
• Solução modular para o problema do
“zoom” (vulgo “tranco-seguido-de-batida”)
– Acrescentar um conector na configuração
• Modelo próximo a execução + verificável
Próximos passos
• Mapeamento para Maude
• Testar o sistema de interlocking
• Model checking