digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
305 stars 40 forks source link

mm1 import cycles don't fail nicely #49

Open ammkrn opened 3 years ago

ammkrn commented 3 years ago

Trying to make two files that import each other (a.mm1 imports b.mm1 and b.mm1 imports a.mm1) stops a future from making progress during elaboration at this await point which I think leads to:

    elab(a.mm1) // waiting on mk(b.mm1)
        elab(b.mm1) // waiting on mk(a.mm1)
          elab(a.mm1) // vfs returns FileCache::InProgress, giving a(2nd) a sender handle from a(1st) 

and the receiver seems to await a message that isn't coming. You either get the last parser error before it picked up the completed import, or the logging shows no error and gets stuck on "change a.mm1" if you copy-paste the whole line.

adding the previously seen/parent path info as an argument to server::elaborate seems like an easy way to propagate the relevant info without changing any types. Server/VFS are convenient, but neither of those seem concerned with the actual content of files.

digama0 commented 3 years ago

I guess the easiest way to detect this would be if the version of the InProgress is the same as the requested elaboration. Currently we check the version in case the current request is older than the one in progress, in which case we join on the newer in progress work, but if the versions are equal then I think we have to be in an import cycle.

ammkrn commented 3 years ago

That seems right to me. The only thing I could think of was downstream changes, but it looks like those are handled after elaboration is finished.

digama0 commented 3 years ago

On review, I don't think this will work. I added basic cycle detection in a9af014, but it is still possible to get into deadlocks if you start multiple elaborations in parallel:

(1) open a.mm1
(2) open b.mm1
thread 1: start elab a.mm1 for (1)
thread 1: mark a.mm1 as in progress
thread 1: (3) a.mm1 depends on b.mm1
thread 2: start elab b.mm1 for (2)
thread 2: mark b.mm1 as in progress
thread 2: (4) b.mm1 depends on a.mm1
thread 1: start elab b.mm1 for (3)
thread 1: b.mm1 is in progress, call stack says a.mm1 -> b.mm1 so no cycle, block on thread 2
thread 2: start elab a.mm1 for (4)
thread 2: a.mm1 is in progress, call stack says b.mm1 -> a.mm1 so no cycle, block on thread 1

I think a more significant change is required to make it deadlock free - a global incremental cycle checker similar to the one used for ParserEnv::add_coe_raw.