661133 - Verifier phase1 suffers from a badly sorted worklist

Status: RESOLVED WONTFIX

(Tamarin Graveyard :: Verifier, defect, P2)

Description

[Edwin Smith]

During phase 1, the verifier iterates to a fixed point while checking the code, using a worklist algorithm.  The worklist is not sorted, so it is possible for a block to be revisited far more often than necessary.

If the ABC basic blocks are roughly in reverse postorder, then this problem is worst when the blocks in the worklist are in high-to-low abc order.

Comment 1

[Edwin Smith]

Attachment: vprof probes to count verifyBlock() calls during phase 1

Comment 2

[Edwin Smith]

Attachment: Patch to keep the worklist sorted in abc order.

Comment 3

[Edwin Smith]

Comment on attachment 536594 [details] [diff] [review]
Patch to keep the worklist sorted in abc order.

stats on biggest 100 AS3 swfs in brightspot (well, my copy of it):

            #visits  #blocks  visits/block
            -------  -------  ------------
  baseline: 752954   407190   1.85
  with fix: 736368   407190   1.81

Now compare this with scimark2.swf:

            #visits  #blocks  visits/block
            -------  -------  ------------
  baseline: 459582   894      514.1
  with fix: 34538    894      38.6

Still not great (38, vs 1.8 for typical AS3 code), but better.

Comment 4

[Edwin Smith]

Attachment: default notNull for int/uint/Number/bool = true

It turns out the main cause of re-queues is int-typed variables
changing from notNull=true -> false.  Really, the notnull bit doesn't
apply to integers, so we need to force them =true for numbers or
just ignore the bool.

this patch makes them true by default but doesn't force them.  I think
there still is noise with uint, but the requeues are way down:

             #visits  #blocks  visits/block
             -------  -------  ------------
  baseline:  459582   894      514.1
  fix 1:      34538   894       38.6
  fix 1+2:     7764   894        8.7

Comment 5

[Edwin Smith]

Comment on attachment 536594 [details] [diff] [review]
Patch to keep the worklist sorted in abc order.

Just looking for general feedback; the improvements in these two patches are solid on the example swfs.

This visit order assumes the ABC is approximately ideal (nearly reverse postorder) because I didn't want to add the complexity of really finding the CFG and really visiting in reverse postorder.  However, if we did that, the asymptotic time would probably go down even more. 

I'm looking for Alchemy feedback on how much effort is worth it.

Comment 6

[Tamarin Bot]

changeset: 6492:4d0f5d485a2f
user:      Ruchi Lohani<[e-mail]>
summary:   Bug 661133 - Verifier phase1 suffers from a badly sorted worklist (review pending, push=rulohani)

http://hg.mozilla.org/tamarin-redux/rev/4d0f5d485a2f

Comment 7

[Steven Johnson]

Looks like it was pushed with DOPROF defined -- probably want to doublecheck

Comment 8

[William Maddox]

Comment on attachment 536594 [details] [diff] [review]
Patch to keep the worklist sorted in abc order.

Keeping the worklist sorted is a good idea on the face of it, and the measured results show it is effective when using visits/block as the metric.  How much are we losing in execution time due to the insertion sort, however?  I'd like to see the average execution time for Brightspot -Dverifyonly as well as for scimark2.swf.  I have no idea, BTW, what our average worklist length looks like.

Comment 9

[William Maddox]

Comment on attachment 536869 [details] [diff] [review]
default notNull for int/uint/Number/bool = true

This is a cheap fix for a big win on scimark2.swf.  I would expect this fix to benefit typical cases as well.  We could replace the switch in typeNotNull()
with a table lookup (array indexed by builtin type), but that may not be worth the trouble.

Comment 10

[Edwin Smith]

Comment on attachment 536594 [details] [diff] [review]
Patch to keep the worklist sorted in abc order.

I'm surprised these were pushed already!  requesting post-mortem review

Comment 11

[Felix S. Klock II [:pnkfelix, :fklock]]

(In reply to comment #10)
> Comment on attachment 536594 [details] [diff] [review] [diff] [details] [review]
> Patch to keep the worklist sorted in abc order.
> 
> I'm surprised these were pushed already!  requesting post-mortem review

I don't understand why they were pushed.  I'll email Ruchi.

Tommy's backed it out from TR, I'm planning to do the same for TR-sec.

Comment 12

[Felix S. Klock II [:pnkfelix, :fklock]]

(In reply to comment #11)
> Tommy's backed it out from TR, I'm planning to do the same for TR-sec.

For the record, Tommy's backout happened in:

changeset:   6493:9591c3bd25b4
user:        Tommy Reilly <[e-mail]>
date:        Fri Jul 29 13:18:50 2011 -0400
summary:     Backed out changeset 4d0f5d485a2f
http://hg.mozilla.org/tamarin-redux/rev/9591c3bd25b4

Comment 13

[William Maddox]

Comment on attachment 536594 [details] [diff] [review]
Patch to keep the worklist sorted in abc order.

Review of attachment 536594 [details] [diff] [review]:
-----------------------------------------------------------------

The code looks good, except for the minor nits that 'requeue' and 'pathologically' are misspelled. I'm giving this an R-, though because my concerns in comment 8 have not been addressed.

Comment 14

[Edwin Smith]

This is probably low hanging fruit for Dolores

Comment 15

[Edwin Smith]

Attachment: vprof probes to count verifyBlock() calls during phase 1

Updated instrumentation patch

Comment 16

[Sylvestre Ledru [:Sylvestre]]

Tamarin is a dead project now. Mass WONTFIX.

Comment 17

[Sylvestre Ledru [:Sylvestre]]

Tamarin isn't maintained anymore. WONTFIX remaining bugs.