843   this assumption is awkward to formalise in our model. There are mainly 

   843   this assumption is awkward to formalise in our model. There are mainly 

   844   two reasons: First, we do not specify what ``running'' the code of a 

   844   two reasons: First, we do not specify what ``running'' the code of a 

   845   thread means, for example by giving an operational semantics for

   845   thread means, for example by giving an operational semantics for

   846   machine instructions. Therefore we cannot characterise what are ``good''

   846   machine instructions. Therefore we cannot characterise what are ``good''

   847   programs that contain for every looking request also a corresponding

   847   programs that contain for every looking request also a corresponding

   851   Therefore we

   852   Therefore we

   852   leave it out and let the programmer assume the responsibility to

   853   leave it out and let the programmer assume the responsibility to

   853   program threads in such a benign manner (in addition to causing no 

   854   program threads in such a benign manner (in addition to causing no 

   854   circularity in the RAG). In this detail, we do not

   855   circularity in the RAG). In this detail, we do not

   855   make any progress in comparison with the work by Sha et al.

   856   make any progress in comparison with the work by Sha et al.