SISTEMAS OPERACIONAIS PROVA 0.1 AN OUTCAST OF THE ISLANDS

RAUL H.C. LOPES

1. Introdução

Esta parcial da prova 0 avalia seu conhecimento de sincronização de processos. A prova é individual. Você pode consultar as suas nostas de aula, seu livro, outros professores, a mãe, o pai e o vizinho, mas não o namorado e nem o Senhor do Castelo: a leitura e entendimento da prova faz parte do processo de avaliação.

Todas as questões têm o mesmo peso.

2. Notação

Como convencionado em sala de aula, vale a seguinte notação:

• Atribuição simultânea de a para x e b para y.

x , y : = a , b

• Seqüência

P

; Q

• Concorrente P || Q

• atômico

$< P > $

• atômico e bloqueante até que B seja verdadeiro: < B → S >

3. As questões

Considere as definições de L.Lamport para safety e liveness. Saftey: bad things don’t happen. Liveness: Good things do happen.

Date: 13/03/2003.

Questão 1. Identifique condições de safety e liveness para o problema de readers and writers. Você nao precisa prová-las, mas justifique-as informalmente.

Questão 2. Uma variante do seguinte algoritmo de exclusão mútua foi apresentada em sala e identificada como incorreta. Identifique suas condiçoes de safety e liveness do algoritmo a seguir, estabelecendo:

• Possíveis alterações que devam ser feitas para que essas condições sejam satisfeitas.

• Condições de correção do algoritmo: invariantes, condições de progresso, limites de variáveis, etc.

|[ || i : i ∈ {0, 1} :

y . i = t r u e
; x . i , v : = t r u e , i

; < not ( y . i ) ∨ v=ī → s k i p >

; CS . i
; y . i , x . i : = f a l s e , f a l s e

]|

Questão 3. Uma variante do seguinte algoritmo de exclusão mútua foi apresentada em sala. Identifique as condiçoes de safety e liveness do algoritmo a seguir, estabelecendo:

• Alterações mínimas que devam ser feitas para que essas condições sejam satisfeitas.

• Condições de correção do algoritmo: invariantes, condições de progresso, limites de variáveis, etc.

|[ || i : i ∈ {0, 1} :

n . i = 1
; n . i : = n . ī + 1

; w h i l e ( n.ī ≠ 0 ∧ n.ī ≤ n.i)

; CS . i
; n . i := 0

]|