Quais são as vantagens da linearizabilidade como uma propriedade de segurança? Existem alguns resultados com base nesse fato na literatura?
Suponha que você implementou uma máquina de memória compartilhada que só satisfaz eventual linearização , definidos da seguinte forma: em cada corrida α de M , existe algum ponto no tempo T α , tal que linearização detém de tempos T α diante. Note que não há nenhuma ligado na parte superior T . (*) (Trata-se de uma contrapartida artificial da definição de propriedade de segurança padrão de linearizabilidade.)MαMTαTαT
Essa implementação de memória compartilhada não seria muito útil para o programador: observe que, se houver apenas linearidade possível, não há garantias quanto à consistência das operações de leitura / gravação em qualquer prefixo "inicial" de uma execução (antes do tempo desconhecido) ). Ou, em outras palavras, o que aconteceu até agora, você ainda pode estender o prefixo atual de uma execução para uma que satisfaça a eventual linearização. T
(*) Se houvesse esse limite superior, a eventual linearização passaria a ser uma propriedade de segurança.
Como caracterizar linearidade como conjuntos fechados topologicamente? Em particular, qual é o conjunto subjacente e qual é a topologia?
Podemos definir uma topologia de métrica no conjunto , que é o conjunto de todas as possíveis execuções de um algoritmos distribuídos. Observe que cada execução α ∈ A S S N C corresponde a uma sequência infinita de transições de estado. Para α , β ∈ A S Y N C , α ≠ β , nós definimos d ( α , β ) : = 2 - N , onde NA SYNCα ∈ A SYNCα , β∈ A SYNCα ≠ β
d( α , β) : = 2- N
Né o índice mais antigo em que as transições de estado em
e
β diferem; caso contrário, se
α = β , definimos
d ( α , β ) = 0 .
αβα = βd( α , β) = 0
O primeiro argumentam que é uma métrica em Um S Y N C . Por definição, d é não-negativo e ∀ α , β ∈ A S Y N C temos
d ( α , β ) = d ( β , α ) . Para α , β , y ∈ A S Y N C , o triângulo-desigualdade d ( α , βdA SYNCd∀ α , β∈ A SYNCd( α , β) = d( β, α )α , β, γ∈ A SYNC se mantém trivialmente se γ = α ou
γ = β . Consideremos agora o caso em que d ( α , γ ) ≥ d ( γ , β ) > 0 , isto é,
d ( α , γ ) = 2 - n 1 e d ( γ , βd( α , β) ≤ d( α , γ) + d( γ, β)γ= αγ= βd( α , γ) ≥ d( γ, β) > 0d( α , γ) = 2- n1 1 , para alguns índices
n 1 ≤ n 2 . Como γ compartilha um prefixo comum de comprimento n 2 - 1 com β, mas apenas um prefixo de comprimento n 1 - 1 com α , segue que α e
β diferem no índice n 1 e, portanto, d ( α , β ) = d ( α , γ )d( γ, β) = 2- n2n1 1≤ n2γn2- 1βn1−1ααβn1d(α,β)=d(α,γ)e a desigualdade de triângulo segue. O caso em que segue analogicamente.0<d(α,γ)<d(γ,β)
As métricas induz uma topologia (por exemplo, a página 119 de [1]), onde o ε -balls B ε ( α ) = { β ∈ A S Y N C | d ( α , β ) < ε } são os conjuntos abertos básicos . Agora, discutiremos por que as propriedades de segurança correspondem a conjuntos fechados: Se uma execução α não satisfaz uma propriedade de segurança
S ⊆ A S S N C , isto é, \ α ∉ SdϵBε(α)={β∈ASYNC∣d(α,β)<ε}αS⊆ASYNCα∉S, Então há um índice
, onde todas as execuções de p que partilham um prefixo maior que N com α não estão em S . Isso corresponde à intuição, uma vez que uma propriedade de segurança é violada no prefixo de uma execução, não faz diferença como esse prefixo é estendido!
Formalmente, suponha que alfa ∉ S . Existe um N ≥ 0 tal que, se algum
β ∈ A S Y N C tiver d ( α , β ) < 2NβNαSα∉SN≥0β∈ASYNCou seja,αe
βcompartilhar um prefixo de comprimento≥N, entãoβ∉S. Assim, o conjunto de execuçõesSé fechado, pois seu complemento é aberto.d(α,β)<2−N,αβ≥Nβ∉SS
[1] James Munkres. Topologia.
The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...
?Com relação à sua primeira pergunta - as propriedades de segurança são, de certa forma, as propriedades "mais fáceis" de lidar, com relação a problemas como verificação e síntese de modelos.
A razão básica para isso é que, na abordagem teórica dos autômatos aos métodos formais, o raciocínio sobre propriedades de segurança se reduz ao raciocínio sobre traços finitos, o que é mais fácil do que a configuração padrão de traços infinitos.
Veja o trabalho de Orna Kupferman aqui como ponto de partida.
fonte