microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

Concrete levels can include non-external atomic methods #21

Closed jaylorch closed 3 years ago

jaylorch commented 3 years ago

The concrete-level checker doesn't raise an error if the level contains an {:atomic} method that isn't {:extern}. But it should, since the compiler can't compile an {:atomic} method (at least, not so that its calls and returns are indeed nonyielding points).