[Agda] Fwd: Hashtables: 'Basic' hashtables performance quirks on Win64

Andreas Abel abela at chalmers.se
Sat Jan 18 12:25:41 CET 2014


Found this message on libraries at haskell.org...

I guess Agda is a serious test case for hashing methods.  Last year, I 
had problems with a bad version of the 'hashable' package.

Kyra, none of the main Agda developers uses Windows.  You could help by 
making a patch that conditionally (#if) chooses a hash table 
implemenation that works for your case.

Cheers,
Andreas

-------- Original Message --------
Subject: Hashtables: 'Basic' hashtables performance quirks on Win64
Date: Sat, 18 Jan 2014 13:38:34 +0400
From: kyra <kyrab at mail.ru>
To: Haskell Libraries <libraries at haskell.org>

Having built Agda on 64-bit GHC 7.6.3 on Windows I've stumbled on Agda
being unbearable slow (I tried it on Penryn and Sandy Bridge computers).
The culprit turned out to be Agda uses 'BasicHashTable' in
src/full/Agda/TypeChecking/Serialise.hs (line 98).

Switching either to Cuckoo or Linear immediately cures the problem.

The problem does not manifest itself on 32-bit Windows build or any
Linux build.

Also 'Basic' hashtable perform better than Cuckoo and Linear in standard
benchmarks on Win64. And at the same time in Agda scenario it's
performance degrades by a *couple of orders of magnitude*!

Thus, *all* things are important here: 64-bit, Windows, Agda use case.

I wonder what stands behind this behaviour? What are specifics of
'Basic' hashtable implementation and how to fix this or should this be
fixed at all?

Regards,
Kyra
_______________________________________________
Libraries mailing list
Libraries at haskell.org
http://www.haskell.org/mailman/listinfo/libraries





More information about the Agda mailing list