Bringing Safe, Dynamic Parallel Programming to the SPARK Verifiable Subset of Ada

摘要

SPARK is a verifiable subset of Ada which has been in use for over 20 years for developing the most critical parts of complex real-time applications . A restricted subset of the Ada tasking model is included in the newer versions of SPARK ("RavenSPARK"), but this is a very static model, with a fixed number of tasks and minimal task interaction . In this presentation we will describe an extension of SPARK to support safe highly parallel programming, targeted at the growing number of multicore and manycore processors appearing on the market today.