Aplicações: Leitores – Escritores

Um Piloto Automático (Cruise Control)

Alexandre Sztajnberg

1o Workshop do Projeto VASPDPG-TI CNPq 552192/02-3

Março / 2004IC/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 'Readers, 'Writers ; // readers actually reading boolean 'Writing ; // a writer is writing int 'Want-to-read, 'Want-to-write; // number of potential int 'turn; int R = 0, W = 1;

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çõesa) 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)) (c)(( (Writing = FALSE)) (( Want-to-read = 0) until (Writing = FALSE)))

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)) (d) (( Want-to-read = 0) until (Writing = TRUE))

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

engineOn

engineOff

accelerator

breack

engine loop getThrottle setThrottle getSpeed

enableControl

disableControl

recordSpeed

clearSpeed

correta

sleep 500 setSpeed

carInput

on

off

resume

cruiseInput

carSimulator

speedController

cruiseController

splitter

speedControlPace

carController

tranco

Cruise control configuration

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.

module carInput {

out port oneway () engineOn;

out port oneway () engineOff;

out port oneway () accelerate;

out port oneway () brake;

}

engineOn

engineOff

accelerator

breack

carInput

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.

module controlInput { out port oneway (void) on; out port oneway (void) off; out port oneway (void) resume;}

on

off

resume

cruiseInput

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); } }}

sleep 500

speedControlPace

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; }

in port int (void) getbrakepedal { return brakepedal; }

in port int (void) getSpeed { return speed; }} engine loop

getThrottle setThrottle getSpeed

carSimulator

Conector splitter interaction { brake-in > (brake-out1 || brake-out2); accelerator-in > (accelerator-out1 || accelerator-out2); engineOff-in > (engineOff-out1 || engineOff-out2);

engineOn-in > (engineOn-out1 || engineOn-out2); }} // splitter

engineOn

engineOff

accelerator

breack

carInput

splittercarController

enableControl

disableControl

recordSpeed

clearSpeed

correta

cruiseController

Conector carController

• Controls ignition– Engine instantiation ?– Engine link ?

• Translates the carInput stimulos into engine stimulus

• Avois breacing and accelerating at the same time

engineOnengineOff

acceleratorbreack

carInput splitter

engine loop getThrottle setThrottle getSpeed

carSimulator

carControllerconnector CarController { in port oneway (void) brake; in port oneway (void) accelerator; in port oneway (void) engineOff; in port oneway (void) engineOn; out port oneway (double, int) setTrottle; staterequired double getThrottle; staterequired int getbreakpedal;

exclusive {engineOn, engineOff, accelerate, break} }

interaction { engineOn > guard (ignition == false) { before {ignition = true; // instantiate carSimulator e link carSimulator } alternative (ground); > ground; engineOff > guard (ignition == true) { before {ignition = false; // remove carSimulator } alternative (ground); > ground; accelerate > guard (true) { before { if (_brakepedal = getbrakepedal > 0) _brakepedal=0; else {if (g_throttle=getThrottle<(maxThrottle-1))_throttle += 1.0; else _throttle = maxThrottle; }} > 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

speedController

engineOn

engineOff

accelerator

breack

enableControl

disableControl

recordSpeed

clearSpeed

correta

setSpeed

carInput

on

off

resume

cruiseInput

cruiseController

tranco

connector Controller { int INACTIVE = 0; int ACTIVE = 1; int CRUISING = 2; int STANDBY = 3; int controlState = INACTIVE;

out port oneway () disableControl; out port oneway () enableControl; out port oneway () clearSpeed; out port oneway () recordSpeed;

out port oneway () correta;

exclusive {brake, accelerator, engineOff, engineOn, on, off, resume}

interaction { brake > guard (controlState==CRUISING) { alternative (ground); after {controlState=STANDBY;} } > disableControl;

accelerator > guard (controlState==CRUISING) {

alternative (ground); after {controlState=STANDBY;} } > disableControl; } // end Control

• Componente principal da lógica de interlocking da aplicação

– Máquina de estados verificável no livro

Conector speedController

• Em cruzeiro, este conector efetivamente controla a velocidade do motor, acelerando e desacelerando quando necessário

• uma malha de controle• precisa do speedControlPace para

dar ritmo a este controle

engine loop getThrottle setThrottle getSpeed

enableControl

disableControl

recordSpeed

clearSpeed

correta

sleep 500

carSimulator

cruiseController

speedControlPace setSpeed

speedController

connector SpeedControl { int DISABLED = 0; //speed control states int ENABLED = 1; int state = DISABLED; //initial state int setSpeed = 0; //target cruise control speed staterequired int getSpeed; // getSpeed special port in port oneway (void) recordSpeed; in port oneway (void) clearSpeed; in port oneway (void) enableControl; in port oneway (void) enableControl;

in port oneway (void) setSpeed;

out port oneway (float) setThrottle;

exclusive {recordSpeed; clearSpeed; enableControl; disableControl; setSpeed} }

interaction { recordSpeed > guard (true) {before {setSpeed=getSpeed;}} alternative (ground); > ground; clearSpeed() > guard (state==DISABLED) {before {setSpeed=0;}} alternative (ground); > ground; enableControl() > guard (state==DISABLED) {before {state=ENABLED}}; alternative (ground); > ground; disableControl() > guard (state==ENABLED) {before {state=DISABLED}}; alternative (ground); > ground; setSpeed > guard (state==ENABLED) {before {

error = setSpeed - getSpeed / 6.0; steady = setSpeed / 12.0; } } alternative (ground); > setThrottle(steady+error); //simplified feed back control }}

VerificaçõesSafety 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