Performance of Type Checking

DavePearce commented 7 years ago

Some test cases are taking a long time to verify because of the type checker. It's going extremely slowly at times for reasons unknown. Here are some stats from BoolList_Valid_3:

ASSERT #1...17, 225ms
ASSERT #2...25, 330ms
ASSERT #3...25, 224ms
ASSERT #4...56, 390ms
ASSERT #5...65, 423ms
ASSERT #6...65, 340ms
ASSERT #7...65, 386ms
ASSERT #8...116, 680ms
ASSERT #9...116, 699ms
ASSERT #10...116, 699ms
ASSERT #11...119, 755ms
ASSERT #12...132, 821ms
ASSERT #13...133, 830ms
ASSERT #14...132, 840ms
ASSERT #15...135, 851ms
ASSERT #16...152, 874ms
ASSERT #17...155, 885ms
ASSERT #18...156, 926ms
ASSERT #19...155, 945ms
ASSERT #20...158, 960ms
ASSERT #21...155, 976ms
ASSERT #22...156, 998ms
ASSERT #23...301, 1106ms
ASSERT #24...314, 1181ms
ASSERT #25...314, 1196ms
ASSERT #26...314, 1228ms
ASSERT #27...118, 955ms
ASSERT #28...130, 1011ms
ASSERT #29...130, 1027ms
ASSERT #30...56, 432ms
ASSERT #31...4, 1ms
ASSERT #32...6, 0ms
ASSERT #33...6, 0ms
ASSERT #34...13, 18ms
ASSERT #35...28, 64ms
ASSERT #36...30, 81ms
ASSERT #37...28, 69ms
ASSERT #38...35, 110ms
ASSERT #39...53, 182ms
ASSERT #40...55, 173ms
ASSERT #41...55, 183ms
ASSERT #42...62, 196ms
ASSERT #43...84, 234ms
ASSERT #44...84, 242ms
ASSERT #45...86, 237ms
ASSERT #46...91, 279ms
ASSERT #47...109, 347ms
ASSERT #48...109, 352ms
ASSERT #49...111, 355ms
ASSERT #50...116, 411ms
ASSERT #51...134, 484ms
ASSERT #52...136, 482ms
ASSERT #53...136, 482ms
ASSERT #54...143, 493ms
ASSERT #55...165, 548ms
ASSERT #56...167, 553ms
ASSERT #57...165, 565ms
ASSERT #58...172, 607ms
ASSERT #59...190, 676ms
ASSERT #60...192, 684ms
ASSERT #61...192, 699ms
ASSERT #62...199, 728ms
ASSERT #63...221, 780ms
ASSERT #64...5, 1ms
ASSERT #65...39, 2ms
ASSERT #66...36, 2ms
ASSERT #67...37, 3ms
ASSERT #68...36, 3ms
ASSERT #69...77, 3ms
ASSERT #70...74, 4ms
ASSERT #71...75, 5ms
ASSERT #72...74, 4ms
ASSERT #73...77, 5ms
ASSERT #74...86, 14ms
ASSERT #75...86, 9ms
ASSERT #76...3, 0ms
ASSERT #77...6, 25ms
ASSERT #78...6, 38ms
ASSERT #79...4, 0ms
ASSERT #80...5, 31ms
DONE

The first column is the number of subtype operations, and the second is the overall time for that assert to be type checked. The generic stats are:

Parsed 1 source file(s). ...................................................... [101ms+5mb]
Typed 1 source file(s). ................................................... [36594ms-452mb]

DavePearce commented 7 years ago

Here's another good example:

WARNING: version numbering unavailable
Parsed 1 source file(s). ....................................................... [73ms+3mb]
Typed 1 source file(s). ................................................... [56755ms-132mb]
Verified 1 source file(s). ................................................ [12847ms-149mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) ......................................... [69678ms-279mb]

So, type checking takes four times as long as verification ... what the ???

DavePearce commented 7 years ago

Another interesting case:

bash-3.2$ wy compile --verify --wyaldir=. --verbose Complex_Valid_7.whiley 
WARNING: version numbering unavailable
Parsed 1 source file(s). ....................................................... [37ms+1mb]
Typed 1 source file(s). ........................................................ [28ms+1mb]
Generated code for 1 source file(s). ........................................... [49ms+1mb]
[/Users/djp/projects/WhileyTheoremProver/./Complex_Valid_7.wyil] applied coercion check  [1ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [130ms-2mb]
Wyil => Wyal: compiled 1 file(s) ............................................... [52ms+2mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). .................................................... [6241ms-162mb]
Verified 1 source file(s). ................................................. [1389ms-164mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) .......................................... [7630ms-327mb]

DavePearce commented 7 years ago

And another:

[/Users/djp/projects/WhileyTheoremProver/./ConstrainedList_Valid_3.wyil] applied coercion check  [1ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [127ms-2mb]
Wyil => Wyal: compiled 1 file(s) ............................................... [48ms+1mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). ..................................................... [5457ms-45mb]
Verified 1 source file(s). .................................................. [1328ms+19mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) ........................................... [6785ms-26mb]

DavePearce commented 7 years ago

bash-3.2$ wy compile --verify --wyaldir=. --verbose ConstrainedList_Valid_20.whiley 
WARNING: version numbering unavailable
Parsed 1 source file(s). ....................................................... [33ms+1mb]
Typed 1 source file(s). ........................................................ [26ms+1mb]
Generated code for 1 source file(s). ........................................... [47ms+1mb]
[/Users/djp/projects/WhileyTheoremProver/./ConstrainedList_Valid_20.wyil] applied coercion check  [0ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [121ms-2mb]
Wyil => Wyal: compiled 1 file(s) ............................................... [44ms+1mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). .................................................... [1913ms-244mb]
Verified 1 source file(s). .................................................. [428ms+136mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) .......................................... [2341ms-107mb]

DavePearce commented 7 years ago

[/Users/djp/projects/WhileyTheoremProver/./ConstrainedList_Valid_23.wyil] applied coercion check  [0ms]
Whiley => Wyil: compiled 1 file(s) ............................................ [133ms-2mb]
Wyil => Wyal: compiled 1 file(s) ............................................... [58ms+2mb]
Parsed 1 source file(s). ............................................................ [0ms]
Typed 1 source file(s). .................................................... [17245ms-45mb]
Verified 1 source file(s). ................................................. [3582ms-260mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) ......................................... [20828ms-305mb]

DavePearce commented 7 years ago

Notes

Disabling checkIsSubtype() has no effect on performance.
Fixing isApplicable() to return true leads to a 10x reduction in performance.

Confirmed this with both ConstraintList_Valid_23 and Complex_Valid_7.

One possible reason that isApplicable() is causing problems is potentially because NameResolution is expensive. Each call to isApplicable() is not super long-running. Normally say 2ms but occasionally up to 19ms.

More points:

NameResolver Caching. Caching of resolve() calls does reduce the number of times that resolution is actually performed, but is not reducing overall performance at all. My guess is that this is coming from WyalFile enclosing = loadModule(nid,name); in resolveAll().
loadModule(). We can rule out the possibility that this is related to reading files from disk. Basically, I don't think it is because it's always resolving with the enclosing file.
resolveAll(). Even with caching enabled this isn't having much effect. After caching there we only 8 individual calls made accounting for maybe 20ms in total.

DavePearce commented 7 years ago

Right, am not making lots of progress here. So, this is the best information so far:

Parsed 1 source file(s). ....................................................... [77ms+3mb]
************ STATS
HITS: 0
MISSES: 0
RESOLVE: 354ms
RESOLVEALL: 1248ms
******************
Typed 1 source file(s). ..................................................... [9147ms-55mb]
Verified 1 source file(s). .................................................. [5805ms+69mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) .......................................... [15034ms+18mb]

It doesn't look like either of those are the real problem here. That would rule out WyalFileResolver. Some more stats related to CoerciveSubtypeOperator.isSubtype():

=========== STATS ==============
CALL COUNT: 4913
WORKLIST COUNT: 34453
WORKLIST SIZE: 36708
================================

This counts: the number of calls to isSubtype(), the number of calls to isVoid(ArrayList,Worklist,BitSet) and the cumulative size of the worklist on each of those calls.

The above stats do look a bit odd if we consider the type being queried in that file:

type Matrix is ((int[])[] rows) where ...

This doesn't involve any unions or other things which might cause complication. I suppose we might expect a depth of three for that type, leading to say 4913 * 3 = 14739 calls.

DavePearce commented 7 years ago

The following loop ...

for (int i = 0; i != truths.size(); ++i) {
    Atom<?> ith = truths.get(i);
    for (int j = i + 1; j != truths.size(); ++j) {
        Atom<?> jth = truths.get(j);
        if (isVoidAtom(ith, jth, assumptions)) {
           time += (System.currentTimeMillis() - start);
            return true;
        }
    }
}

... is only accounting for around 1385ms in this example. Doesn't seem to be the main contributing factor. That is still a lot of time unaccounted for.

One interesting observation is that the BitSet assumptions is very big because of the number of SyntacticElements in the given file. Caching the creation of this BitSet gives the following timing:

Typed 1 source file(s). .................................................... [3716ms-384mb]
Verified 1 source file(s). ................................................. [2724ms-143mb]
Generated code for 1 source file(s). ................................................ [0ms]
Wyal => Wyail: compiled 1 file(s) .......................................... [6518ms-524mb]

For the allValidVerification test suite, this reduces the time from around 45ms to 37ms. Or, 152ms to 126ms if we remove the ignores on those too long for travis.

UPDATE: using HashSetAssumptions leads to better overall performance. This requires only 56ms if we remove the ignores on those too long for travis.

DavePearce commented 7 years ago

Resolved and released in v0.6.0

Whiley / WhileyTheoremProver

Performance of Type Checking #110

Notes