Reader/Writer Property Specifications as Never Claims

This page describes the reader/writer properties as Never Claims. For other property specification formalisms, click on the name of the property.

Exclusive-write property

never {
  do
    :: writer__1[writer_1_pid]@state_2 & 
       writer__2[writer_2_pid]@state_2 -> goto accept
    :: else -> skip 
  od;
  accept:
    do
      :: skip
    od
}
	

Write-first property

never {
  do
    :: ( wrote == true ) -> break
    :: reader__1[reader_1_pid]@state_2 -> goto accept
    :: else -> skip
  od;
  do
    :: skip
  od;
  accept:
    do
      :: skip
    od;
}
	

Back to Readers/Writers

Back to main