Detecção de Deadlock em Especificações Algébricas para Sistemas Concorrentes
Autores
|
1659 |
Marcelo Sihman
|
407,273
|
|
1660 |
407,273
|
Informações:
Publicações do PESC
Detecção de Deadlock em Especificações Algébricas para Sistemas Concorrentes
Marcelo Sihman
Agosto/1998
| Orientador: | Mário Roberto Folhadela Benevides | |
| ||
Esta tese apresenta um estudo detalhado de dois formalismos, CCS e
PI-Calculus (Cálculos de Processos), e de especificações de sistemas concorrentes
sincronizados nos mesmos. Também estudamos conceitos de sistemas distribuídos,
algoritimos de sincronização e detecção de deadlock.
Neste trabalho, nós propomos um algoritimo para geração automática de
especificações formais em CCS (Calculus of Communicating Systems) para Problemas
de Compartilhamento de Recursos como o dos Filósofos Jantando. Nós apresentamos
uma solução para o caso geral e também para duas variantes particulares: alta
carga e casos em anel. Para cada uma, nós estudamos os aspectos combinatoriais
do número de estados necessários para cada especificação. Esta especificação
é sincronizada utilizando um mecanismo chamado Escalonamento por Reversão de
Arestas SER. O uso do SER garante que a especificação gerada pelo algoritmo tem,
por construção, algumas propriedades desejáveis como exclusão mútua, ausência de
bloqueio perpétuo (deadlock), ausência de espera indefinida (starvation), execução
ótima para o caso em que vizinhos alternam operação, e para o caso em que uma
implementação completamente distribuída pode ser usada. CCS é a inspiração de
alguns formalismos baseados em álgebra como o PI-Calculus, e também de linguagens
para especificação formal como o LOTOS. O algoritimo apresentado aqui poderia ser
facilmente adaptado para a maioria destes formalismos e ferramentas de especificação.
Nós também apresentamos um algoritmo para detecção de deadlock em especificações
álgebricas para sistemas concorrentes. Todos os possíveis caminhos de execução
da especificação são simulados e caso exista algum tipo de deadlock possível de
ocorrer durante sua execução este é detectado pelo algoritmo e informado ao usuário.
Nosso algoritmo atua sobre um agente composto em CCS ou PI-Calculus, que, na
maioria dos casos, possui determinadas portas restritas a comunicações internas
entre seus agentes componentes. Quando uma pessoa for executar uma especifição
poderá testá-la antes para saber se ela está livre de deadlock.
Deadlock Detection in Algebraic Specifications for Concurrent Systems
Marcelo Sihman
August/1998
| Advisor: | Mario Roberto Folhadela Benevides | |
| Department: Systems Engineering and Computer Science | ||
This thesis presents a detailed study of two formalisms, CCS and PI-Calculus
(Process Calculi), and of synchronized specifications for concurrent systems. We
also study concepts of distributed systems, scheduling algorithms and deadlock detection.
In this work, we propose an algorithm for automatic generation of formal
specifications in CCS (Calculus for Communicating Systems) for Resource Sharing
Problems like the Dining Philosophers. We present a solution for the general case
and also for two particular variants: heavy-load and ring cases. For each one, we
study the combinatorial aspects of the number of states needed in each specification.
This specification is synchronized using a mechanism called Scheduling by Edge
Reversal SER. The use of SER guarantees that the specification generated by the
algorithm has, by construction, some desirable properties such as mutual exclusion,
absence of deadlock, absence of starvation, concurrency-wise optimality given the
requirement that neighbors alternate, and the case with which a fully distributed
implementation can be carried out. CCS is the inspiration of some algebraic based
formalism like the Pi-Calculus, and also of languages for formal specification like
LOTOS. The algorithm presented here could be easily adapted for most of these
specification formalisms and tools.
We also present an algorithm for deadlock detection in algebraic specifications
for concurrent systems. All the possible execution paths of the specification are
simulated and in the case that there is the possibility of ocurrence of some kind
of deadlock during its execution this is detected by the algorithm and informed to
the user. Our algorithm works over a composed agent in CCS or PI-Calculus, that, in
most of the cases, has restrictions applied over some specific ports, destined only
to internal communication among its component agents. When one wants to execute a
specification he will be able to test it before to know if it is deadlock free.