Concurrent data structure: Difference between revisions

Revision as of 12:38, 23 November 2009

Revision as of 12:43, 23 November 2009

Line 42:

</ref><ref name="sahni"/>. Most notably, in a sequential environment

one specifies the data structure's properties and checks that they

are implemented correctly, by providing '''[[[[[Linear Temporal Logic#safety property|safety properties''']]. In

a concurrent environment, the specification must also describe

'''liveness properties''' which an implementation must provide.

Safety properties usually state that something bad never happens,

while liveness properties state that something good keeps happening.

These properties can be expressed, for example, using [[linearLinear Temporal Logic]].

temporal logic]].

The type of liveness requirements tend to define the data structure.