• Apresentação
• Avisos e Sumários
• Bibliografia
• Avaliação
  • Grupos
  • Projecto 1
  • Projecto 2
  • Projecto 3
  • Projecto 4
  • Projecto 5
  • Projecto 6
  • Projecto 7
• Material de Apoio
• Contactar Docente

Exclusão Mútua Distribuída

Pretende-se implementar um algoritmo de exclusão mútua distribuído, ou seja sem nenhum controlador centralizado. O mesmo será baseado no conceito token ring. As diversas unidades funcionais estão ligadas através de um anel de comunicação onde circula uma marca. Sempre que uma unidade pretende entrar na zona crítica deverá retirar esta marca do anel, devendo a mesma ser propagada para a unidade seguinte quando não for necessária. A seguinte imagem apresenta um esquema da rede de Petri que modela este problema, para o caso em que temos três unidades funcionais, estando uma delas detalhada.



Cada unidade é constituída por dois módulos. O primeiro, cuja rede se encontra detalhada, representa o componente que pretende usar o recurso crítico. Tem três estados possíveis: Idle, quando está a realizar tarefas que não envolvem o recurso crítico; Waiting, quando está à espera de usar o recurso crítico; e Critical, quando está na zona de exclusão mútua. O segundo é o controlador que irá implementar o protocolo, e cuja especificação é o objectivo deste projecto.

A comunicação entre os dois componentes é feita assincronamente usando os lugares Req (request), Prm (permission), e Rdy (ready). O primeiro é usado para sinalizar a vontade de usar o recurso crítico. O segundo é usado pelo controlador para dar autorização ao outro componente para entrar na zona crítica, e o último serve para este indicar que já terminou a utilização do recurso crítico. O controlador também tem acesso ao anel onde circula a marca. Sempre que deseje, pode retirar a mesma da sua porta de entrada (Tok) ou transferi-la para a unidade funcional que lhe sucede no anel.

Algumas das propriedades que a solução deve verificar são:

• Não existem duas unidades simultaneamente na zona crítica.
• Não existem deadlocks.
• Não existe mais do que uma marca a circular no anel.
• Qualquer unidade que pretenda utilizar o recurso crítico poderá eventualmente fazê-lo.
• Uma unidade não poderá utilizar o recurso crítico duas vezes seguidas se outra unidade também o pretender utilizar.
• A marca não deve circular desnecessariamente pelo anel. Só o deverá fazer se alguma unidade requisitar o acesso à zona crítica.

Para poder satisfazer esta última propriedade poderá ser necessário adicionar um segundo anel de comunicação (com sentido inverso) onde circulam pedidos para libertar a marca.

Notas

Este problema deve ser modelado usando redes de petri e a ferramenta de verificação de modelos SMV. Na modelação deve começar por usar uma rede colorida e depois fazer a seu expansão para uma rede normal. Nesta operação pode começar por usar capacidades e arcos inibidores, que depois deverão ser eliminados usando as regras de transformação ensinadas. As propriedades enumeradas devem ser verificadas pelo modelo a apresentar. Sempre que possível devem ser demonstradas usando técnicas estruturais (como invariantes de lugar), mas também usando verificação de modelos. Para tal terão que ser traduzidas em fórmulas CTL equivalentes. Se desejarem podem enriquecer a especificação adicionando novas características ao modelo ou novas propriedades para verificar. Naturalmente, tal será valorizado na nota final.