[Agda-dev] More efficient handling of TopLevelModuleNames

[Guilhem Moulin]

On Wed, 03 Dec 2014 at 10:11:02 +0100, Nicolas Pouillard wrote:
> On 12/02/2014 11:15 PM, Andreas Abel wrote:
>> A 128bit hash seems to be an alternative to a String representation of
>> TopLevelModuleNames which could lead to a significant speed up of
>> serialization.
>
> I support the choice of 128bit hash. As much as one can experiment with
> different hash functions to test performances. I would recommend choosing
> SHA256 truncated to 128bits. Another option would be to look at SHA3 which
> is faster (if I recall well) and secure as well.

Actually SHA-512 can be faster than SHA-256 on 64 bits platforms [1],
essentially because the word size is larger.  But anyway, the common
cryptographic hash functions (MD5 and SHA-{1,2,3}) were optimized for
large messages, while I guess a typical QId will hardly be longer than,
say 128 bytes.

I'm unsure how significant the overhead would be, but one may want to
benchmark BLAKE2 (derived of BLAKE, a SHA-3 finalist) which

  “is extremely fast both when hashing a single large file and when
   hashing many small files. For example, BLAKE2s hashes 64-byte files
   quicker than SHA-1, MD5, and even MD4.” — https://blake2.net/

-- 
Guilhem.

[1] https://community.emc.com/community/edn/rsashare/blog/2010/11/01/sha-2-algorithms-when-sha-512-is-more-secure-and-faster
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: Digital signature
Url : http://lists.chalmers.se/pipermail/agda-dev/attachments/20141203/74d29fec/attachment.bin