Go up to Top Go forward to Logic Versus Programming

Introduction

• Concurrent algorithm typically described by a program.
  • Correctness of algorithm means program satisfies desired property.
• TLA = Temporal Logic of Actions.
  • Lamport, 1994.
  • Both algorithm and property are specified by formulas in single logic.
  • Correctness of algorithm means algorithm implies property.
• Reasonable to abandon programing language?
  • Mostly reasoning about concurrent algorithms.
  • Concurrent programs are much to complicated.
  • 1 page algorithm = 5000 lines of C code.
  • Goal to detect algorithmic errors.

Talking about concurrent algorithms!