[go: up one dir, main page]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Missing optimization when Kernel Term Sharing is disabled. #555

Merged
merged 1 commit into from
May 29, 2017
Merged

Missing optimization when Kernel Term Sharing is disabled. #555

merged 1 commit into from
May 29, 2017

Conversation

ppedrot
Copy link
Member
@ppedrot ppedrot commented Apr 12, 2017

This patch adds a missing optimization in the kernel. When reducing terms without Kernel Term Sharing set, we don't have to perfom in-place updates because we actually know that there is none on the stack.

This is somewhat critical in UniMath which abuses the flag. I ran the bench three times on it and got the following results:

┌──────────────┬─────────────────────────┬─────────────────────────────────────┬─────────────────────────────────────┐
│              │      user time [s]      │             CPU cycles              │          CPU instructions           │
│              │                         │                                     │                                     │
│ package_name │     NEW     OLD PDIFF   │           NEW           OLD PDIFF   │           NEW           OLD PDIFF   │
├──────────────┼─────────────────────────┼─────────────────────────────────────┼─────────────────────────────────────┤
│  coq-unimath │ 1130.24 1247.54 -9.40 % │ 3132128571062 3456741122915 -9.39 % │ 5332501952654 5812131583426 -8.25 % │
└──────────────┴─────────────────────────┴─────────────────────────────────────┴─────────────────────────────────────┘

Note that I did not bench the other packages because several seemed to be half-broken by the merge of EConstr, and furthermore this optimization is irrelevant to them.

@ppedrot
Missing optimization when Kernel Term Sharing is disabled.
71d7155 
We don't have to perfom in-place updates because we actually know that there
is none on the stack. This should speed up UniMath.
@mortberg mortberg mentioned this pull request Apr 13, 2017
Closed
@maximedenes maximedenes reopened this May 28, 2017
maximedenes
maximedenes approved these changes May 29, 2017
View reviewed changes
Copy link
Member
@maximedenes maximedenes left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems safe to me. The introduction of Zupdate is already guarded by a condition on !share.

@coqbot coqbot merged commit 71d7155 into coq:trunk May 29, 2017
@ppedrot ppedrot deleted the unset-zip-sharing branch May 29, 2017 13:56
@Zimmi48 Zimmi48 modified the milestone: 8.7 Jul 21, 2017
@Zimmi48 Zimmi48 added the kind: performance Improvements to performance and efficiency. label Aug 5, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maximedenes maximedenes maximedenes approved these changes

Assignees
No one assigned
Labels
kind: performance Improvements to performance and efficiency.
Projects
None yet
Milestone
8.7+beta1
Development

Successfully merging this pull request may close these issues.
4 participants
@ppedrot @maximedenes @Zimmi48 @coqbot