I see. Linear types is a way to statically determine which operations are independent of which other operations (and can therefore be run in parallel). That is what I mean by "Ideally, if one knew the effects of all sub-operation generated by a contract many call sequences (whose semantics are sequential) could be run in parallel." in Concurrency, BFS vs DFS (and a proposal)
What I propose in that thread is to be optimistic and run in parallel, check after the execution whether there are concurrency conflicts, and re-run if necessary. This technique is simple and works both for BFS and DFS.
