0004733: Optimisation in bytecomp/simplif.ml leads to memory blowup in coq

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0004733

OCaml

OCaml general

public

2009-02-27 11:41

2012-09-25 20:10

Reporter

bacam

Assigned To

xleroy

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

unable to reproduce

Platform

OS Version

Product Version

3.11.0

Target Version

Fixed in Version

Summary

0004733: Optimisation in bytecomp/simplif.ml leads to memory blowup in coq

Description

Recently I discovered that a particularly demanding file in our coq development (due to the way in which we use coq's module system) compiled in under 1.5GB using the native code version build with -g, but exceeded the maximum 32bit process size (~3GB) using the native code version without -g.

I've tracked this down by trail and error to the optimisation of Llet(Alias, v, l1, l2) in bytecomp/simplif.ml when v only appears once. However I'm not sure exactly which part of the coq source triggers the problem, or if it can be easily solved. (Or if it's even reasonable to blame it on ocamlopt!)

Tags

No tags attached.

Attached Files

Relationships

Notes
(0006352) xleroy (administrator) 2011-12-17 11:01	Another PR that has been dormant for too long, sorry about that. bytecomp/simplif.ml was significantly revised this summer to fix issues that may or may not be related (see PR#5205, PR#5288). So my questions are: - Is this still a problem? especially with the svn trunk version of OCaml? - If so, could we get a repro case?

(0006824) xleroy (administrator) 2012-01-27 12:22	Unable to reproduce. I move to close this PR unless new information is added.

Issue History
Date Modified	Username	Field	Change
2009-02-27 11:41	bacam	New Issue
2009-04-29 15:37	doligez	Status	new => assigned
2009-04-29 15:37	doligez	Assigned To	=> xleroy
2011-12-17 11:01	xleroy	Note Added: 0006352
2011-12-17 11:01	xleroy	Status	assigned => feedback
2012-01-27 12:22	xleroy	Note Added: 0006824
2012-01-27 12:22	xleroy	Status	feedback => resolved
2012-01-27 12:22	xleroy	Resolution	open => unable to reproduce
2012-09-25 20:10	xleroy	Status	resolved => closed