Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 124
    • Issues 124
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 15
    • Merge Requests 15
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #432

Closed
Open
Opened Jan 16, 2020 by Guillaume Melquiond@melquionOwner3 of 4 tasks completed3/4 tasks

Why3 uses too much memory

This is a meta-issue to summarize all the discussions into a single place.

Things to do:

  • Do not precompute Decl.d_sysms, as they consume about 15% memory.
  • Change split_vc so that it introduces premises by itself instead of relying on introduce_premises. The latter has too little information to share common declarations between subtasks. This should make the memory consumption linear rather than quadratic in the number of proof obligations.
  • Investigate Decl.known_add_decl, as its Mid.union call seems responsible for about 25% memory consumption.
  • Investigate Termcode.task_v3, as its Mid.add call seems responsible for about 25% memory consumption.

Remark: The master branch supports memory profiling, when using a suitable compiler, e.g., the one from the Opam switch 4.07.1+statistical-memprof. First, configure Why3 with --enable-statmemprof and build it. Then, execute bin/why3ide -L examples/multiprecision examples/multiprecision/toom. Once the interface is loaded, execute sturgeon-connect in Emacs to see the memory consumption. (See Statmemprof's documentation for details about Sturgeon.)

Edited Feb 11, 2020 by MARCHE Claude
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#432