[Agda-dev] More efficient handling of TopLevelModuleNames

[Dominique Devriese]

I may still be missing something, but are we sure that *cryptographic*
hashes are needed?  Why not a simpler (and probably faster),
non-cryptographic hash function, like

  http://en.wikipedia.org/wiki/Java_hashCode()#The_java.lang.String_hash_function
?

Regards,
Dominique


2014-12-03 21:18 GMT+01:00 Guilhem Moulin <guilhem.moulin at chalmers.se>:
> 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
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>