The reason that a formal model didn't arrive is because it's impossible; the foundation of concurrency is the ability to change state and return the previous state atomically (even if it is only one bit/byte; xref cmpxchg). This necessarily makes the system non deterministic. So building a base for concurrency from synchronous tasks is impossible unless those synchronous tasks are atomic from start to end; most tasks are more than one op code long.