#4265: Sanity bug found by +RTS -DS in Agda
-------------------------------+--------------------------------------------
Reporter: wkahl | Owner:
Type: bug | Status: infoneeded
Priority: normal | Milestone:
Component: Runtime System | Version: 6.13
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Linux | Blocking:
Architecture: x86_64 (amd64) | Failure: Runtime crash
-------------------------------+--------------------------------------------
Comment(by wkahl):
Get the development versions of Agda and its standard library today (they
will probably start changing a lot next week):
{{{
mkdir AGDADIR
cd AGDADIR
darcs get --lazy http://code.haskell.org/Agda
darcs get --lazy http://www.cs.nott.ac.uk/~nad/repos/lib/
}}}
Install Agda:
{{{
cd AGDADIR/Agda
ghc --make Setup
./Setup configure --prefix=AGDA_INSTDIR -p --ghc-option=-dcore-lint
./Setup build -v
./Setup install
cd main/src
ghc --make Setup
./Setup configure --prefix=AGDA_INSTDIR -p --ghc-options="-dcore-lint
-debug -rtsopts"
./Setup build -v
./Setup install
}}}
Then typecheck one of the standard library modules (this is the first that
I found that produced the error, and the second I tried):
{{{
export PATH="AGDA_INSTDIR/bin:$PATH"
cd AGDADIR/lib/src
time agda +RTS -DS -C0 -i0 -K64M -M12G -H12G -S -RTS -i .
Relation/Binary/Product/Pointwise.agda
}}}
For me, this produces:
{{{
...
658434064 89664904 90883176 6.61 6.64 197.93 201.76 0 0 (Gen:
1)
Checking Relation.Nullary.Product
(/var/tmp/AGDA/2010-08-23/lib/src/Relation/Nullary/Product.agda).
5628117344 57015040 143382872 5.39 5.42 229.71 233.67 0 0
(Gen: 0)
agda: internal error: ASSERTION FAILED: file rts/sm/Sanity.c, line 664
(GHC version 6.13.20100815 for x86_64_unknown_linux)
Please report this as a GHC bug:
http://www.haskell.org/ghc/reportabug
Aborted
real 3m59.170s
user 3m54.805s
sys 0m3.743s
}}}
This first run produces lots of {{{.agdai}}} files; even when running
again without deleting these, I get:
{{{
...
22634296 3761736 35310416 3.30 3.30 66.85 70.15 0 0 (Gen:
0)
34169504 4645712 37974760 3.32 3.32 70.34 73.65 0 0 (Gen:
0)
Skipping Function.Equality
(/var/tmp/AGDA/2010-08-23/lib/src/Function/Equality.agdai).
Skipping Relation.Binary.PropositionalEquality
(/var/tmp/AGDA/2010-08-23/lib/src/Relation/Binary/PropositionalEquality.agdai).
Skipping Data.Unit (/var/tmp/AGDA/2010-08-23/lib/src/Data/Unit.agdai).
agda: internal error: ASSERTION FAILED: file rts/sm/Sanity.c, line 664
(GHC version 6.13.20100815 for x86_64_unknown_linux)
Please report this as a GHC bug:
http://www.haskell.org/ghc/reportabug
Aborted
real 1m17.233s
user 1m13.547s
sys 0m3.649s
}}}
For installing Agda, getting the intermediate packages involves bumping
some upper bounds in the cabal dependency declarations; I have:
{{{
$ ghc-pkg list
/usr/local/packages/ghc-6.12.3/lib/ghc-6.12.3/package.conf.d
Agda-2.2.7
Cabal-1.8.0.6
HTTP-4000.0.9
QuickCheck-2.1.1.1
array-0.3.0.1
base-3.0.3.2
base-4.2.0.2
bin-package-db-0.0.0.0
binary-0.5.0.2
bytestring-0.9.1.7
containers-0.3.0.0
darcs-2.4.4
dataenc-0.13.0.3
directory-1.0.1.1
dph-base-0.4.0
dph-par-0.4.0
dph-prim-interface-0.4.0
dph-prim-par-0.4.0
dph-prim-seq-0.4.0
dph-seq-0.4.0
extensible-exceptions-0.1.1.1
ffi-1.0
filepath-1.1.0.4
ghc-6.12.3
ghc-binary-0.5.0.2
ghc-prim-0.2.0.0
hashed-storage-0.4.13
haskeline-0.6.2.2
haskell-src-1.0.1.3
haskell98-1.0.1.1
hpc-0.5.0.5
hscolour-1.17
html-1.0.1.2
integer-gmp-0.2.0.1
mmap-0.4.1
mtl-1.1.0.2
network-2.2.1.7
old-locale-1.0.0.2
old-time-1.0.0.5
parsec-2.1.0.1
pretty-1.0.1.1
process-1.0.1.3
random-1.0.0.2
regex-base-0.93.2
regex-compat-0.93.1
regex-posix-0.94.2
rts-1.0
syb-0.1.0.2
template-haskell-2.4.0.1
terminfo-0.3.1.2
time-1.1.4
unix-2.4.0.2
utf8-string-0.3.6
xhtml-3000.2.0.1
zlib-0.5.2.0
}}}
By the way, the first standard library module I tried produced a different
effect I had not seen before:
{{{
$ time agda +RTS -DS -C0 -i0 -K64M -M12G -H12G -S -RTS -i .
Relation/Binary.agda
...
60672488 24807144 48305448 3.60 3.61 71.59 75.14 0 0 (Gen:
0)
13641288 51824 355384 3.13 3.13 74.76 78.31 0 0 (Gen:
1)
4096 0.00 0.00
8,130,662,960 bytes allocated in the heap
127,438,312 bytes copied during GC
22,124,928 bytes maximum residency (4 sample(s))
203,480 bytes maximum slop
12501 MB total memory in use (195 MB lost due to fragmentation)
Generation 0: 6 collections, 0 parallel, 19.95s, 20.80s elapsed
Generation 1: 4 collections, 0 parallel, 12.00s, 14.47s elapsed
INIT time 0.00s ( 0.00s elapsed)
MUT time 42.81s ( 43.05s elapsed)
GC time 31.95s ( 35.27s elapsed)
EXIT time 0.00s ( 3.13s elapsed)
Total time 74.80s ( 78.36s elapsed)
%GC time 42.7% (45.0% elapsed)
Alloc rate 189,713,958 bytes per MUT second
Productivity 57.3% of total user, 54.7% of total elapsed
Warning: 4100 bytes at 0x1e52430 still allocated at shutdown
Warning: 4100 bytes at 0x1e07b00 still allocated at shutdown
Warning: 4100 bytes at 0x1e06af0 still allocated at shutdown
Warning: 4100 bytes at 0x1df15c0 still allocated at shutdown
real 1m18.724s
user 1m14.803s
sys 0m3.546s
}}}
Again, these warnings persist on the re-run with the previously generated
{{{.agdai}}} files still there.
(But with different addresses at each attempt.)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4265#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
