parallelize interface serialization

[UlfNorell]

From sanzhi...@gmail.com on May 23, 2013 06:07:39

Interface serialization can take ~25-30% of the time of typechecking a module, and especially for the module currently being loaded in emacs it'd be great if it could be completed in the background while handling user's commands concurrently.

Are there any obvious showstoppers for this? Otherwise I'd be willing to investigate further and implement it.

It's somewhat related to #688 but simpler because serialization doesn't use the typechecker.

Original issue: http://code.google.com/p/agda/issues/detail?id=855

[UlfNorell]

From nils.anders.danielsson on May 23, 2013 04:21:30

Are there any obvious showstoppers for this?

I don't see any (but note that both the TCM monad and the serialiser use IORefs). Just make sure that interface files are written atomically.

Otherwise I'd be willing to investigate further and implement it.

Great!

Status: Accepted
Labels: Type-Enhancement

[UlfNorell]

From nils.anders.danielsson on May 23, 2013 04:22:26

It's somewhat related to #688

"Emacs mode fails on Windows"?

[UlfNorell]

From sanzhi...@gmail.com on May 23, 2013 04:30:18

Sorry, 668

[UlfNorell]

From andreas....@gmail.com on May 23, 2013 06:58:00

You meant issue 668 (ah, now we have a clickable link). ;-)

[UlfNorell]

From sanzhi...@gmail.com on June 10, 2013 17:55:17

I've reappeared with two questions:

1) On line 375 of Agda.Interaction.Imports:

                  -- We skip the file which has just been type-checked to                                                                          
                  -- be able to forget some of the local state from                                                                                
                  -- checking the module.                                                                                                          
                  -- Note that this doesn't actually read the interface                                                                            
                  -- file, only the cached interface.                                                                                              
                  skip file

How does "skip file" manages to do that? I ask mostly to make sure I don't destroy the effect.

2) Is it acceptable to drop the invariant that the cached Interface is only valid if it's more recent than a corresponding written one? The motivation is that with concurrency we might need the cached one when we haven't yet written it down, and once written the cached version would still have an older timestamp. We'd check that the cached version is more recent than the source file, instead.

I've also attached a preliminary patch implementing the parallelization but it seems we could streamline isCached, skip and their use because there's still some overlapping.

Attachment: issue-885_-write-interfaces-in-parallel.dpatch

[UlfNorell]

From nils.anders.danielsson on June 14, 2013 09:34:06

How does "skip file" manages to do that?

I wonder if this comment is incorrect. I think the point of using skip is to get increased sharing (via the hash-consing in Agda.TypeCheecking.Serialise). Feel free to improve the comment.

Is it acceptable to drop the invariant that the cached Interface is only valid if it's more recent than a corresponding written one? The motivation is that with concurrency we might need the cached one when we haven't yet written it down, and once written the cached version would still have an older timestamp. We'd check that the cached version is more recent than the source file, instead.

I don't think we should use time stamps at all (see issue 178 ).

[UlfNorell]

From sanzhi...@gmail.com on June 14, 2013 16:38:51

If that's what skip is supposed to do then we should change line 274 of Agda.Interaction.Imports from "if mt < t" to "if mt <= t" otherwise it returns the cached version when called just after typechecking the module.

[UlfNorell]

From nils.anders.danielsson on June 17, 2013 02:28:03

If that's what skip is supposed to do then we should change line 274 of Agda.Interaction.Imports from "if mt < t" to "if mt <= t" otherwise it returns the cached version when called just after typechecking the module.

The use of skip is a bit of a hack, and Interaction.Imports is hard enough to understand as it is. I suggest that we change the code so that it is easier to understand. One part of this change could be to enforce the invariant that the "decoded" modules are actually always decoded (deserialised); I don't think that this invariant holds at the moment.

[UlfNorell]

From sanzhi...@gmail.com on June 17, 2013 03:23:22

One part of this change could be to enforce the invariant that the "decoded" modules are actually always decoded (deserialised); I don't think that this invariant holds at the moment.

It doesn't in fact, modules typechecked in the current run go into "decoded" without that step.

Enforcing this invariant prevents parallelizing serialization though, afaict.

[UlfNorell]

From ulf.nor...@gmail.com on November 08, 2013 01:09:14

I tried this patch and there seems to be some problems:

A minor one is that there's race when compiling using MAlonzo (maybe the other compilers as well) where the compiler expects the interface file to exist and crashes if it hasn't yet been written.

A more serious problem is that parallelisation doesn't seem to buy any performance. Checking the standard library with -N4 has my cpu working at around 250% but checking takes 5% longer real time than before. I've got

Before patch: 3m23s After patch: -N4 3m35s (real) 6m18s (cpu) -N1 3m42s

Status: InfoNeeded

[UlfNorell]

From ulf.nor...@gmail.com on November 08, 2013 01:25:12

Actually, that doesn't seem to be a problem with this patch. Without the patch running on 4 cores exhibits exactly the same behaviour. Of course, I would have expected things to be faster with the patch...

[UlfNorell]

From ulf.nor...@gmail.com on November 08, 2013 01:45:46

It looks like simply adding -threaded to the compiler flags is responsible for the 20s slowdown when running on a single core.

[UlfNorell]

From sanzhi...@gmail.com on November 08, 2013 06:03:03

How have you measured the time? If done in batch mode it's not actually measuring the main effect of the patch.

The patch only parallelizes for the --interaction mode, and even then it can only make use of 2 cores because the serializations are done in-order.

It was a fairly conservative attempt to gain responsivity in the emacs mode, rather than to improve overall performance.

Though I also realized that the common case during development, i.e. reloading the same file with some holes in it, doesn't actually involve any interface writing so this attempt is probably not going to have a big impact on the interaction case either.