TICC-paradigm to build formally verified parallel software for multi-core chips

摘要

This invention teaches a way of implementing formally verified massively parallel programs, which run efficiently in distributed and shared-memory multi-core chips. It allows programs to be developed from an initial abstract statement of interactions among parallel software components, called cells, and progressively refine them to their final implementation. At each stage of refinement a formal description of patterns of events in computations is derived automatically from implementations. This formal description is used for two purposes: One is to prove correctness, timings, progress, mutual exclusion, and freedom from deadlocks/livelocks, etc. The second is to automatically incorporate into each application a Self-Monitoring System (SMS) that constantly monitors the application in parallel, with no interference with its timings, to identify and report errors in performance, pending errors, and patterns of critical behavior. This invention also teaches a way of organizing shared-memory for multi-processors that minimizes memory interference, protects data and increases execution efficiency.