Einar Broch Johnsen, University of Oslo An abstract behavioral model of distributed concurrent objectsAbstract Concurrency remains a major challenge for program verification. In particular, the multithread concurrency model of today's mainstream object-oriented languages poses severe obstacles for reasoning about programs. Concurrent objects offer an alternative concurrency model for object-orientation which seems better suited for highly parallel, distributed or multicore architectures, and which supports compositional program verification. We discuss features of concurrent objects in the context of Creol, an executable modeling language designed for reasoning about distributed concurrent objects, highlighting central aspects of its design philosophy, operational semantics, type theory, and proof theory. |
|
|
