I may be incorrect, but my impression was that concurrent systems formalization (at least, in ways that are actually relevant on real hardware) was still an area of very active research. Is saying they exist meaningful even in a strictly theoretical sense?