runtimeverification / runtimeverification/haskell-backend

[Haskell-Performance] Performance Drop Using Cell-Map despite deterministic map accesses

Open
#3,569 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

performance
Dominant language
Haskell
Stars
224
Forks
43
PR merge metrics
No merged PRs in 30d

Description

Please Prepare Test Data

Program Execution in a definition where the <k> cell resides under a cell with multiplicity * and type Map results in a rise in time per rewrite step as the configuration grows dynamically.

Consider the following definition:

module MULTICELL
  imports INT
  syntax Stmt ::= "addCell" "(" Int ")"  | "wait"

  configuration <cells>
                  <cell multiplicity="*" type="Map">
                    <id> 0 </id>
                    <k> $PGM:Stmt </k>
                  </cell>
                </cells>
                <counter> 1 </counter>


  rule <k> addCell(N) => addCell(N -Int 1) ... </k>
       (.Bag =>  <cell> <id> C </id> <k> wait </k> </cell> )
       <counter> C => C +Int 1 </counter>
    requires N >Int 0

  rule addCell(0) => .

endmodule

A program in the above definition has the form addCell(N), where N is the number of <cell>(s) to be added during execution. Note that none of the added cells can be further rewritten; only the initial cell is rewritten. Thus, the access to the map is deterministic.

Attached are bug reports for programs addCell(70) and addCell(80). On my machine, the former takes 31 s, and the latter 54 s, indicating rewrites take much longer as the size of the cell map increases.

P.S. I also tried added <id> 0 </id> to the rules for addCell, in the hope that it would speed up identifying the map-item where the rule can apply, but it didn't seem to make any difference.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the MULTICELL definition in the issue and reproduce the behavior using the attached addCell(70) and addCell(80) bug reports. Compare rewrite time as the Map cell collection grows; done means the performance regression is characterized and the reported scaling behavior is addressed.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
backend, performance
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.