[Agda] .agdai serialisation runs into segfault in Data.HashTable

[Wolfram Kahl]

I just filed the GHC ticket appended below:

  http://hackage.haskell.org/trac/ghc/ticket/4805

I succeeded localising one of my segfaults in
Agda.TypeChecking.Serialise.encode,
and by exchanging the use of Data.HashTable there with Data.Map,
got rid of the segfault.

I attach the patch with my changes to Agda.TypeChecking.Serialise.

I did not touch the decode part, and I noticed that ``Int'' values
are ``encoded'' as single Int32 values, which is, in general,
not appropriate on a 64-bit machine.
I inserted a test there, and, so far, have not seen any truncating
Int-encodings, but this deserves at least more documentation.
I also inserted a warning every time ``fresh'' goes over 2^30 ---
but currently I have no reason to believe that this could become a real issue
in the near future...

Wolfram

----- Forwarded message from GHC <cvs-ghc at haskell.org> -----

From: "GHC" <cvs-ghc at haskell.org>
Precedence: bulk
Cc: glasgow-haskell-bugs at haskell.org
Auto-Submitted: auto-generated
Date: Mon, 29 Nov 2010 23:18:37 -0000
Reply-To: glasgow-haskell-bugs at haskell.org
Subject: [GHC] #4805: segfault in Data.HashTable, triggered by long Agda runs

#4805: segfault in Data.HashTable, triggered by long Agda runs
-------------------------------+--------------------------------------------
    Reporter:  wkahl           |       Owner:                         
        Type:  bug             |      Status:  new                    
    Priority:  normal          |   Component:  libraries/base         
     Version:  7.0.1           |    Keywords:  Data.HashTable segfault
    Testcase:                  |   Blockedby:                         
          Os:  Linux           |    Blocking:                         
Architecture:  x86_64 (amd64)  |     Failure:  Runtime crash          
-------------------------------+--------------------------------------------
 Agda uses {{{Data.HashTable}}} for interface (*.agdai) serialisation.

 I have been able to localise a reproducible segfault (with one of the many
 theories in a sizeable Agda develoment) in
 {{{Agda.TypeChecking.Serialise.encode}}} inside the {{{icode}}} call,
 which essentially limits the possible source of the segfault to the Agda
 module {{{Agda.TypeChecking.Serialise}}} and to {{{Data.HashTable}}}.

 Then I replaced all hash table uses in {{{encode}}} with {{{Data.Map}}},
 and the Agda run in question finishes successfully.
 (I confirmed with a selection of the theories that already could be type-
 checked with {{{Data.HashTable}}} that the {{Data.Map}}}-based version
 generates the same interface files.)

 (Agda interface serialisation maintains four partial maps; their
 respective sizes at the end of this run are 151796,733,3319,0.)

 I consider this as a (non-constructive) proof that there is a bug in
 {{{Data.HashTable}}}.

 (For the time being, I need to make some long-delayed progress in my Agda
 developments and won't have time to try to debug {{{Data.HashTable}}}, but
 I should be able to occasionally test potential fixes.)


 Wolfram

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4805>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
----- End forwarded message -----
-------------- next part --------------
A non-text attachment was scrubbed...
Name: switch_encode_to_Data.Map.patch.gz
Type: application/x-gzip
Size: 8941 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20101129/da5632a0/switch_encode_to_Data.Map.patch.gz