CakeML/cakeml

The encoders are _big_

Open

#793 opened on Oct 15, 2020

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Standard ML (98 forks)auto 404
dev experienceenhancementgood first issuehigh reward

Repository metrics

Stars
 (1,169 stars)
PR merge metrics
 (PR metrics pending)

Description

Some numbers from a --target=riscv --exp_cut=99999 build (9a0180e sexpr-bootstrap):

1069060 cml_x64Prog_x64_enc_5306
 990976 cml_arm7Prog_arm7_enc_5296
 938348 cml_riscvProg_riscv_enc_5348
 784956 cml_arm8Prog_arm8_enc_5342
 373572 cml_mipsProg_mips_enc_5352
 291168 cml_ag32_enc_5324

Some of this is probably unavoidable with heap-allocated words but looking at the HOL input to the translator in riscvProgScript and x64ProgScript we seem to be forcing the encoders into a highly canonical form where no logic can be shared between different instructions; particularly notable are the 16 reg/imm (not)(lower, less, equal, test) cases of JumpCmp which result in 16 copies of the logic to encode a conditional jump displacement. Improving the pre-translate conversions here could make the bootstrap significantly faster with no effect whatsoever on compiling things in the logic.

Contributor guide

Research direction
Identify where logic is duplicated in the encoder, particularly for JumpCmp's 16 reg/imm cases. Examine the pre translate conversion steps in riscvProgScript and x64ProgScript to see how canonicalization prevents sharing. Propose changes to allow sharing without affecting correctness.
Tech stack
None
Domain
backend
Issue type
Performance
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
4
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
3-5 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
CakeMLcompiler backendHOL
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30