Opened 9 years ago

Closed 8 years ago

#4805 closed bug (invalid)

segfault in Data.HashTable, triggered by long Agda runs

Reported by: wkahl Owned by:
Priority: normal Milestone: 7.2.1
Component: libraries/base Version: 7.0.1
Keywords: Data.HashTable segfault Cc: hackage.haskell.org@…
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: Runtime crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (6)

comment:1 Changed 9 years ago by wkahl

Currently, I normally run with the following RTS flags:

 +RTS -C0 -i0 -K64M -M12G -H12G -S -RTS 

comment:2 Changed 9 years ago by liyang

Cc: hackage.haskell.org@… added

comment:3 Changed 9 years ago by simonmar

Milestone: 7.0.3
Status: newinfoneeded

Can you give us instructions to reproduce the problem, even if it involves compiling Agda?

comment:4 Changed 9 years ago by simonpj

Which version of GHC was this? There was a bug in 6.12 which seg-faulted sometimes with very large heaps. We can't make progress on this without more info.

Simon

comment:5 Changed 9 years ago by wkahl

This should have been 7.0.1 - I'll try to reproduce this after Feb. 21.

comment:6 Changed 8 years ago by igloo

Resolution: invalid
Status: infoneededclosed

Please reopen if you have a way to reproduce this.

Note: See TracTickets for help on using tickets.