Contents 1 Introduction 284 1.1 General Motivation.......·..···· ··。 286 1.2 Overview....... 289 2 Background 291 2.1 Linearizability.... .·.291 2.2 Progress Properties.··· 293 2.3 Contextual Refinement and Abstraction Theorems.....297 2.4 Verifying Progress Properties................303 3 Basic Technical Settings 313 3.1 The Language················ 313 3.2 Execution Traces and Fairness of Scheduling.·:····· 319 4 Linearizability and Contextual Refinement 322 4.1 Linearizability 322 4.2 Contextual Refinement and Abstraction····. 324 5 Progress Properties 325 5.1 Progress for Objects with Total Methods Only.······ 325 5.2 Progress for Objects with Partial Methods..··.··.·327Contents 1 Introduction 284 1.1 General Motivation . . . . . . . . . . . . . . . . . . . . . 286 1.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 2 Background 291 2.1 Linearizability . . . . . . . . . . . . . . . . . . . . . . . . 291 2.2 Progress Properties . . . . . . . . . . . . . . . . . . . . . 293 2.3 Contextual Refinement and Abstraction Theorems . . . . . 297 2.4 Verifying Progress Properties . . . . . . . . . . . . . . . . 303 3 Basic Technical Settings 313 3.1 The Language . . . . . . . . . . . . . . . . . . . . . . . . 313 3.2 Execution Traces and Fairness of Scheduling . . . . . . . . 319 4 Linearizability and Contextual Refinement 322 4.1 Linearizability . . . . . . . . . . . . . . . . . . . . . . . . 322 4.2 Contextual Refinement and Abstraction . . . . . . . . . . 324 5 Progress Properties 325 5.1 Progress for Objects with Total Methods Only . . . . . . . 325 5.2 Progress for Objects with Partial Methods . . . . . . . . . 327