Add a Strategy command for ucmra and cmra projections

Investigate timing consequences of adding a Strategy command. Motivation was the following example:

From iris.algebra Require Import frac_auth agree numbers auth.
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Import proofmode.

Strategy expand [ucmra_cmraR ucmra_equiv ucmra_dist ucmra_pcore ucmra_op ucmra_valid ucmra_validN ucmra_ofe_mixin ucmra_cmra_mixin].

Section weird_slow_qed.               (* using UR here *)
  Lemma slow_qed `{!inG Σ (frac_authUR $ optionUR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (Some $ to_agree n)) ⊢ own γ1 (●F (Some $ to_agree n)).
  Proof. time iIntros "$". Time Qed. (* 0.2 seconds -> now 0.01 *)

                                      (* using R here *)
  Lemma fast_qed `{!inG Σ (frac_authUR $ optionR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (Some $ to_agree n)) ⊢ own γ1 (●F (Some $ to_agree n)).
  Proof. time iIntros "$". Time Qed. (* instant *)

                                      (* using UR here *)
  Lemma slow_qed2 `{!inG Σ (frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (●F (to_agree n))) ⊢ own γ1 (●F (●F (to_agree n))).
  Proof. time iIntros "$". Time Qed. (* 1.4 seconds! -> now 0.044 *)

                                       (* using R here *)
  Lemma fast_qed2 `{!inG Σ (frac_authUR $ frac_authR $ agreeR $ natO)} γ1 (n : nat) : 
        own γ1 (●F (●F (to_agree n))) ⊢ own γ1 (●F (●F (to_agree n))).
  Proof. time iIntros "$". Time Qed. (* instant *)

  (* Note that if proven with `reflexivity`, Qed also becomes instant *)
End weird_slow_qed.

where Strategy offers a drastic performance improvement.

changed the description

Timing run started, results will appear at the below URLs

• examples
• iron
• lambda-rust
• gpfsl

It gives serious performance improvements on individual files in gpfsl, e.g., -30% on gpfsl-examples/lock/proof_ticket_lock_gps.v, and no performance regressions.

Let's try the version where we also have strategy for cmra.

added 1 commit

• 6e1e6cea - Add Strategy command for cmra

Compare with previous version

Alright, I added a similar Strategy command for cmra, let's see :)
For future reference:

• proof_ticket_lock_gps.v was using UR where R would suffice, here
• mono_list_list.v sped up by 28%, but I am not sure why
• proof_hw_graph.v sped up by 11%, and was also using UR where R would suffice, e.g. here

Re-run data will appear at:

• examples
• iron
• gpfsl
• lambda-rust

The additional Strategy command for cmra does not seem to have much effect on performance for these projects. My initial guess was that people apparently do not write tyR if tyO suffices. But the blowup in unification time also seems much smaller than what happens for ucmra:

From iris.algebra Require Import frac_auth agree numbers auth list.
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Import proofmode.


Section weird_slow_qed.
  Lemma cmra_ofe_10 `{!inG Σ $ agreeR $ optionR $ optionR $ optionR $ optionR $ optionR $ optionR $ optionR $ optionR $ optionR $ optionR $ natO} γ (n : nat) :
    own γ (to_agree $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some n) ⊢ 
    own γ (to_agree $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some n).
  Proof. time iIntros "$". Time Qed. (* 0.02 *)

  Lemma cmra_ofe_11 `{!inG Σ $ agreeR $ optionO $ optionO $ optionO $ optionO $ optionO $ optionO $ optionO $ optionO $ optionO $ optionO $ natO} γ (n : nat) :
    own γ (to_agree $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some n) ⊢ 
    own γ (to_agree $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some $ Some n).
  Proof. time iIntros "$". Time Qed. (* 0.005 *)
End weird_slow_qed.

Also note that the Strategy command for ucmra does not actually fix the blowup in unification time, it just makes sure it becomes bad a bit later. The following takes too long to parse without the Strategy, but even with the strategy, Qed. still takes 1.4 seconds.

Lemma slow_qed3 `{!inG Σ (frac_authUR $ frac_authUR $ frac_authUR $ agreeR $ natO)} γ1 (n : nat) : 
      own γ1 (●F (●F (●F (to_agree n)))) ⊢ own γ1 (●F (●F (●F (to_agree n)))).
Proof. time iIntros "$". Time Qed.

Also note that the Strategy command for ucmra does not actually fix the blowup in unification time, it just makes sure it becomes bad a bit later. The following takes too long to parse without the Strategy, but even with the strategy, Qed. still takes 1.4 seconds.

So... what annotations are missing to make that fast? Or is that the wrong question to ask?

We see big speedups for some files in GPFSL, and otherwise little change. What do we want to do with this MR?

I'm fine landing both of these Strategy, but there should be comments explaining why this particular list of definitions gets assigned a different strategy.

I would say it's best to merge this MR, while keeping in mind that it is only a band-aid (i.e. opening some tracking issue about this problem).

So... what annotations are missing to make that fast? Or is that the wrong question to ask?

I suspect just annotations cannot make it fast. I think the question to ask is:

How do we keep type-checking/unification fast for structures (like ofe, cmra and ucmra) that have combinators (like optionUR : cmra → ucmra) and coercions (like ucmra_cmraR : cmra → ucmra), especially when stacking alot of these combinators?

I would say it's best to merge this MR, while keeping in mind that it is only a band-aid (i.e. opening some tracking issue about this problem).

I'm fine with that, but the code does need comments explaining our thinking and how these lists were determined.

mentioned in issue #539

added 265 commits

• 6e1e6cea...f0e490d1 - 262 commits from branch iris:master
• 5b0b111f - Add a strategy command for ucmra projections
• f060e6aa - Add Strategy command for cmra
• aab896fd - Added comment explaining why these particular constants are set to be expanded.

Compare with previous version

marked this merge request as ready

changed title from Add a Strategy command for ucmra projections to Add a Strategy command for ucmra and cmra projections

added 1 commit

• 002d3c96 - Fix typo in issue

Compare with previous version

added 1 commit

• 34918ec9 - Fix missing ucmra_unit, ucmra_ofeO

Compare with previous version

added 1 commit

• 3fd5ba73 - No longer doubly closing comment

Compare with previous version