Reader/Writer Property Specifications as QREs

This page describes the reader/writer properties as Quantified Regular Expressions ( QREs ). For other property specification formalisms, click on the name of the property.

Exclusive-write property

for events { {writer_1_start_write}, {writer_1_stop_write},
             {writer_2_start_write}, {writer_2_stop_write} } 
    
show all executions satisfy

[-{writer_1_start_write}, {writer_2_start_write}]*; 
(
  (
    ( {writer_1_start_write}; 
      [-{writer_2_start_write}, {writer_1_stop_write}]*; 
      {writer_1_stop_write}
    ) 
    |
    ( {writer_2_start_write}; 
      [-{writer_1_start_write}, {writer_2_stop_write}]*; 
      {writer_2_stop_write}
    )
  ); 
  [-{writer_1_start_write}, {writer_2_start_write}]* 
)*
	

Write-first property

for events { {reader_1_start_read}, {any_writer_wrote} }

show no executions satisfy
    
[-{reader_1_start_read} , {any_writer_wrote}]*;
{reader_1_start_read} ;
[{reader_1_start_read} , {any_writer_wrote}]*
	 

Back to Readers/Writers

Back to main