Por que a linearizabilidade é uma propriedade de segurança e por que os conjuntos de propriedades de segurança são fechados?

10

No capítulo 13 "Objetos atômicos" do livro "Algoritmos distribuídos" de Nancy Lynch, a linearizabilidade (também conhecida como atomicidade) provou ser uma propriedade de segurança. Ou seja, sua propriedade de rastreio correspondente é não vazia, prefixada e fechada por limite , conforme definido na Seção 8.5.3. Informalmente, uma propriedade de segurança é frequentemente interpretada como dizendo que alguma coisa "ruim" em particular nunca acontece.

Com base nisso, meu primeiro problema é o seguinte:

Quais são as vantagens da linearizabilidade como uma propriedade de segurança? Existem alguns resultados com base nesse fato na literatura?

No estudo da classificação de propriedade de segurança e propriedade de vivacidade, é sabido que a propriedade de segurança pode ser caracterizada como o conjunto fechado em uma topologia apropriada. No artigo "The Safety-Progress Classification" @ 1993 por Amir Pnueli et al. , uma topologia métrica é adotada. Mais especificamente, uma propriedade Φ é um conjunto de palavras (finitas ou infinitas) sobre o alfabeto Σ . A propriedade A(Φ) consiste em todas as palavras infinitas σ modo que todos os prefixos de σ pertençam a Φ . Por exemplo, se Φ=a+b , entãoA(Φ)=aω+a+bω . Uma propriedade infinitaΠ é definida como umapropriedade de segurançaseΠ=A(Φ) para algumas propriedades finitáriasΦ . A métricad(σ,σ) entre as palavras infinitasσ eσ é definida como 0 se forem idênticas, ed(σ,σ)=2j caso contrário, ondejé o comprimento do prefixo comum mais longo com o qual eles concordam. Com essa métrica, a propriedade de segurança pode ser caracterizada como conjuntos fechados topologicamente.

Aqui vem o meu segundo problema:

Como caracterizar linearidade como conjuntos fechados topologicamente? Em particular, qual é o conjunto subjacente e qual é a topologia?

hengxin
fonte

Respostas:

8

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 NASYNCαASYNCα,βASYNCαβ

d(α,β):=2N
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 ( α , βdASYNCdα,βASYNCd(α,β)=d(β,α)α,β,γASYNC 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(α,γ)=2n1 , para alguns índices n 1n 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(γ,β)=2n2n1n2γn21βn11ααβ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ε(α)={βASYNCd(α,β)<ε}αSASYNCα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αSN0βASYNCou seja,αe βcompartilhar um prefixo de comprimentoN, entãoβS. Assim, o conjunto de execuçõesSé fechado, pois seu complemento é aberto.d(α,β)<2N,αβNβSS

[1] James Munkres. Topologia.

Peter
fonte
Obrigado pela sua resposta. Eu tenho que refletir sobre isso. A propósito, você está se referindo ao livro "Topologia" de James R. Munkres quando diz isso The metric d induces a topology (e.g., page~119 of [1]) where the ϵ-balls...?
Hengxin
Sim, eu adicionei a referência.
Peter Peter
Percebi que você sugeriu uma modificação no título deste post (se eu cometer um erro, ignore este comentário). Antes de tudo, concordo que os dois subproblemas devem ser refletidos no título. No entanto, não estou perguntando sobre " por que a linearizabilidade é uma propriedade de segurança?". Estou perguntando sobre as consequências desse fato. Não sei como modificar o título adequadamente e ignorei essa modificação. Entre em contato se tiver outros comentários ou idéias.
hengxin 28/02
Percebi que a caracterização (prova) da linearizabilidade como conjunto fechado basicamente não tem nada a ver com a noção de pontos de linearização. Parece uma prova mais geral que caracteriza qualquer propriedade de segurança como um conjunto fechado. Perdi algo?
Hengxin
Sim, todas as propriedades de segurança são conjuntos fechados, enquanto as propriedades de animação são conjuntos densos nessa topologia. De fato, toda propriedade (isto é, conjunto de execuções) pode ser expressa como uma conjunção (isto é, interseção) de propriedades de segurança e vivacidade.
Peter
6

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.

Shaull
fonte
u¨
Tenho certeza de que Iv'e viu trabalhos que lidam com linearidade via LTL, pelo menos em casos específicos. Se eu os encontrar, vou comentar.
Shaull
Isso será ótimo. Estou sempre curioso sobre como lidar com a linearizabilidade via LTL, especialmente com a noção de pontos de linearização. Seguindo sua dica, encontro o artigo Provando linearizabilidade com lógica temporal . Vou tentar ler nos dias de hoje. No entanto, não tenho certeza sobre sua qualidade. Fico na expectativa dos seus comentários.
evergrow
Talvez isso seja útil. A julgar pelos autores, este é um artigo sério. Não tenho certeza de quão estreita é a conexão com o LTL.
Shaull 28/02