rgrig / topl

TOPL Runtime Verifier
5 stars 1 forks source link

dacapo benchmarks #15

Open rgrig opened 12 years ago

rgrig commented 12 years ago

Check a few properties on the dacapo test-suite.

rgrig commented 12 years ago

Some observations after a few runs of an instrumented Tomcat.

Running time goes up 6 times. This is bad. A little profiling shows that the bottlenecks seem to be the functional queue and the use of HashMap. The queue has size <=2, so the current implementation can definitely be optimized a lot. This is good. For the HashMap, I have to look into who exactly uses it too much.

rgrig commented 12 years ago

The top two users for HashMap seem to be (1) the isObservable check and (2) adding to the set of active states. Point (1) is again good news because we can certainly reduce constant factors a lot, by going from hashes to bitmaps. Not sure about (2).

rgrig commented 12 years ago

The overhead is about 3.3% when (1) the checker is inactive, and (2) ~3 interfaces of Tomcat are instrumented.

rgrig commented 12 years ago

I started writing properties for each of eclipse, tomcat, h2, batik, jython, pmd.

rgrig commented 12 years ago

We now have 18 properties in total for DaCapo.