Happened-before

Na ciência da computação, a relação happened-before (denotada: $\to$), também referenciada como happens-before (em português, "acontece antes"), é uma relação entre o resultado de dois eventos, de modo que se um evento acontecer antes de outro evento, o resultado deve refletir isso, mesmo que esses eventos sejam na realidade executados fora de ordem (geralmente para otimizar o fluxo do programa). Isto envolve ordenar eventos com base na relação causal potencial de pares de eventos em um sistema concorrente, especialmente sistemas distribuídos assíncronos . Foi formulado pelo cientista da computação estadunidense Leslie Lamport .

A relação happened-before é formalmente definida como a menos estrita ordem parcial em eventos tal que:

• Se os eventos $a$e $b$ocorrem no mesmo processo, $a\to b$se a ocorrência do evento $a$ precedeu a ocorrência do evento $b$.
• Se evento $a$é o envio de uma mensagem e evento $b$é a recepção da mensagem enviada no evento $a$, $a\to b$.

Se dois eventos acontecem em diferentes processos isolados (que não trocam mensagens direta ou indiretamente através de processos de terceiros), então os dois processos são chamados concorrentes, isto é, nem $a\to b$ nem $b\to a$ são verdade.

Se existirem outras relações causais entre eventos num determinado sistema, como entre a criação de um processo e o seu primeiro evento, estas relações também são adicionadas à definição. Por exemplo, em algumas linguagens de programação como Java, Predefinição:Sfn C, C++ ou Rust, pode ser considerada a ocorrência de happened-before se a memória gravada pela instrução A for visível para a instrução B, ou seja, se a instrução A completar sua gravação antes da instrução B inicia sua leitura.

Como todas as ordens parciais estritas, a relação acontecido antes é transitiva, irreflexiva e assimétrica, ou seja:

• $\mathrm{\forall }a,b,c$, se $a\to b$ e $b\to c$, então $a\to c$ (transitividade). Isso significa que para quaisquer três eventos $a,b,c$, se $a$ aconteceu antes $b$, e $b$ aconteceu antes $c$, então $a$ deve ter acontecido antes $c$ .
• $\mathrm{\forall }a,a\nrightarrow a$ (irreflexividade). Isso significa que nenhum evento pode acontecer antes de si mesmo.
• $\mathrm{\forall }a,b,$ se $a\to b$ então $b\nrightarrow a$ (assimetria). Isso significa que para quaisquer dois eventos $a,b$, se $a$ aconteceu antes $b$ então $b$ não pode ter acontecido antes $a$ .

Observemos que a propriedade de assimetria decorre diretamente das propriedades anteriores: por contradição, suponhamos que $\mathrm{\forall }a,b,$ nós temos $a\to b$ e $b\to a$ . Então por transitividade temos $a\to a,$ o que contradiz a irreflexividade.

Os processos que compõem um sistema distribuído não possuem conhecimento da relação happened-before, a menos que utilizem um relógio lógico, como um relógio de Lamport ou um relógio vetorial. Isso permite projetar algoritmos para exclusão mútua e tarefas como depuração ou otimização de sistemas distribuídos e concorrentes.

Veja também

• Condição de corrida
• Modelo de memória Java
• Carimbos de data e hora de Lamport
• Relógio lógico

Referências

• Predefinição:Citar livro