Shared Variables Analyser (SVA)
• Ferramenta desenvolvida pelo Computing
Laboratory (Oxford University)
• Analisa programas concorrentes com variáveis
compartilhadas
– Simula programas através de uma rede processos
CSP
– Análise é realizada por FDR de forma transparente
• Front-end da ferramenta implementado em
Java
Fluxo de SVA
Programa + propriedades
(Shared Variables Language)
input.sva
Java Parser
Representação intermediária
(CSPM)
Compilador escrito
em CSPM
+
Análise de refinamentos
com FDR
Resultado das análises (GUI/log)
output.csp
share2priorities.csp
results
Rodando SVA
• Pré-requisitos: Java 1.6 e FDR2 no PATH
• Pacote da ferramenta (sva.tar)
• Compilador share2priorities.csp
deve estar no diretório
• Rodando interface
– java InterpreterGUI in.sva
• Traduz in.sva para output.csp e roda GUI. Resultados
armazenados em results
Lista de
propriedades
GUI
Informações
de debug
Verificar
propriedades
Programa em SVL
• Tipos são inteiros e booleanos
• Setup:
– atomicidade de expressões
– tamanho máximo dos arrays (estáticos)
– faixa de valores (se ultrapassado exceção é lançada)
• Contém variáveis, constantes e sinais
• É uma lista de processos que podem ser
parâmetrizados por inteiros
• Processo é uma lista de comandos separados por ;
– cada comando é delimitado entre { }
Exclusão Mútua de Hyman
(Setup de SVL)
se expressões
%%atomic_exprs = false
são atômicas
%%sba = 3
tamanho de arrays booleanos e inteiros
%%sia = 0
%%MinI = 0
mínimo e máximo para inteiros
%%MaxI = 3
%%InitI = MinI
valor default para inteiros e booleanos
%%InitB = false
declarações precedidas por %% não
são traduzidas pelo compilador
Exclusão Mútua de Hyman em SVL
variáveis inteiras
int count,t=1;
bool[] b;
sig mutexerror;
array de booleanos
sinal (evento)
P(i) = {iter {b[i] := true;
while !(t = i) do
{while b[3-i] do skip;
t := i
processo
};
count := count + 1;
if count > 1 then sig(mutexerror);
count := count -1;
mesmo
b[i] := false;
que: while
}
true do {}
}
Prog = <P(1),P(2)>
programa
Exclusão Mútua de Hyman
(Representação intermediária)
b[i] := true
while !(t = i) ...
P(i) = Iter.Sq.(
Bassign.(BA.1.i,True),
Sq.(While.(Not.Eq.IVar.I.2.Const.i,
while b[3-i] ...
Sq.(While.(BVar.BA.1.(3-i),Skip),
Iassign.(I.2,Const.i))
t := i
),
Sq.(Iassign.(I.1,Plus.IVar.I.1.Const.1),
count := count + 1
Sq.(Cond.(Gt.IVar.I.1.Const.1,
Sig.mutexerror,Skip),
if count > 0 ...
Sq.(Iassign.(I.1, Minus.IVar.I.1.Const.1),
Bassign.(BA.1.i,False)))
)
count := count =1
)
b[i] := true
)
t=1
Prog = Compile((<<P(1),P(2)>>, (<(IVar.I.2,1)>,<>)))
Verificando Propriedades do Programa
• Validade de expressões booleanas (BEXPR)
– assert always BEXPR in PROGRAM
– assert never BEXPR in PROGRAM
• Presença de sinais durante a execução
– assert nosignal { SIGNALS } in
PROGRAM
• Sinal outofrange
– exceção levantada quando o valor de uma expressão
inteira extrapola os limites especificados
Exclusão Mútua de Hyman
(Propriedades)
• Propriedade em SVL
assert nosignal {outofrange, mutexerror}
in Prog
• Propriedade em CSPM
assert CHAOS(diff(Events,{|outofrangeT,
mutexerrorT|}))
[T= Prog
Exclusão Mútua de Hyman
(Propriedades)
Checking output.csp
Checking
CHAOS(diff(Events,{|outofr
angeT,mutexerrorT|})) [T=
Prog
xfalse
BEGIN TRACE example=0
process=1
bvwriteT.BA.1.2.true.0
breq.BE.1
ivevalT.I.2.1.0
beval.BE.1.true
bvevalT.BA.1.1.false.0
...
mutexerrorT.1
END TRACE example=0 process=1
Log de FDR (results)
Pelo log vemos: (1)
expressões não são
atômicas, (2) leitura e
escrita de variáveis são
atômicas
Debug do log
Exclusão Mútua de Hyman
(Propriedades)
• Propriedade em SVL
assert never (count > 1) in Prog
• Propriedade em CSPM
assert CHAOS(diff(Events,
{|assertionfailedT|})) [T=
Compile((<<P(1), P(2),
Atomic.Cond.(Not.Gt.IVar.I.1.Const.1,Ski
p,Sig.assertionfailed)>>,
(<(IVar.I.2,1)>,<>)))
Exclusão Mútua de Hyman
(Propriedades)
Referências
• A. W. Roscoe. Compiling Shared Variable
Programs into CSP. In Proceedings of PROGRESS
workshop 2001, 2001.
• A. W. Roscoe and D. Hopkins. Sva, a tool for
analysing shared-variable programms. In
Proceedings of AVoCS 2007, pages 177–183,
2007.
• Ferramenta e artigos em
http://web.comlab.ox.ac.uk/activities/concurrenc
y/tools/sva/