Define o comportamento permito em programas multithreaded.
- A aplicação não pode assumir mais que a especificação especifica;
- A implementação não pode garantir menos do que a especificação especifica.
- Escritas em memória;
- Leitura em memória;
- Escritas voláteis em memória;
- Leituras voláteis em memória.
- ...
As escritas/leituras voláteis são realizadas sobre uma variável marcada com a anotação @Volatile.
- Relação de ordem parcial sobre as ações;
- O nome da relação é apenas abstrato, não querendo dizer "acontece antes";
- Axiomas de HB:
- Transitividade:
HB(x, y) e HB(y, z) => HB(x, z); - Program Order: Se x e y são ações da mesma thread, e x está primeiro que y em program order, então
HB(x, y); - Volátil: Se x é uma escrita volátil e y é uma leitura volátil da mesma variável, e y lê o valor escrito po x, então
HB(x, y); não é necessário que x e y sejam da mesma thread; - Locks: Se x é um lock release e y um lock acquire do mesmo lock, então
HB(x, y); - Thread Start: Se x é um thread start e y é a primeira operação dessa thread, então
HB(x, y); - Thread Join: Se x é a última ação de uma thread e y é um thread join com a mesma thread, então
HB(x, y); - Thread Interruption: Se x é uma ação de interruption e y é uma ação que vê essa interrupção, então
HB(x, y).
Se x é uma escrita e y uma leitura, e HB(x, y), e não existe um data race e x é a última escrita relacionada com y, então y lê o valor escrito por x.
Um data race é quando duas ou mais threads acedem ao mesmo recurso concorrentemente, e pelo menos uma é de escrita e nenhuma usa locks:
