Functional Equivalence

(1)

Operationally-based Program Equivalence Proofs using LCTRSs

S_,tefan Ciobˆac˘a Dorel Lucanu Andrei Sebastian Buruian˘a [email protected]

[email protected] [email protected]

Alexandru Ioan Cuza University

WPTE 2021

(2)

Outline

1 Motivation

2 Operational Semantics as LCTRSs LCTRSs

Syntax Semantics Example

3 Defining Program Equivalence

4 Proving Equivalence

5 Application

(3)

Functional Equivalence

Given two programsP andQ:

•do they compute the same output for the same input?

Many applications:

1 Compilation;

2 Optimizations;

3 Refinements.

Many approaches, usually based on Relational Hoare Logic. Fewer results in the area ofoperationally-based equivalence:

•GivenP (in a languageL1) andQ (in a languageL2), isP equivalent toQ?

(4)

Functional Equivalence

Many applications:

1 Compilation;

2 Optimizations;

3 Refinements.

Many approaches, usually based on Relational Hoare Logic. Fewer results in the area ofoperationally-based equivalence:

(5)

Functional Equivalence

Many applications:

1 Compilation;

2 Optimizations;

3 Refinements.

Many approaches, usually based on Relational Hoare Logic.

Fewer results in the area ofoperationally-based equivalence:

(6)

Functional Equivalence

Many applications:

1 Compilation;

2 Optimizations;

3 Refinements.

Many approaches, usually based on Relational Hoare Logic.

Fewer results in the area ofoperationally-based equivalence:

(7)

Outline

1 Motivation

5 Application

6 Discussion

(8)

Logically Constrained Term Rewriting Systems

LCTRSshave rewrite rules of the form

l−→rifφ, wherel,r are terms;φis a logical constraint.

terms can containinterpretedsymbols.

Example

init(n)−→loop(n,2) if>, loop(i×k,i)−→comp ifk>1,

loop(n,i)−→loop(n,i+ 1) if¬(∃k.k>1∧n=i×k).

LCTRSs are parametric in a theory (such as LIA, RA, BV, Theory of Arrays, etc.).

(9)

Logically Constrained Term Rewriting Systems

Example

(10)

Logically Constrained Term Rewriting Systems

Example

(11)

Syntax of Programming Language as Order-Sorted Signatures

FunBody ::= Exp|λId.FunBody Stack ::= []|Exp Stack Cfg ::= hStack,Env,Funcsi Env ::= Array{Int}{Int}

Funcs ::= Array{Id}{FunBody}

•Sorts are the nonterminals.

•Language constructs are operations.

•The distinguished sortCfgis the sort ofprogram configurations.

(12)

Syntax of Programming Language as Order-Sorted Signatures

(13)

Syntax of Programming Language as Order-Sorted Signatures

(14)

Syntax of Programming Language as Order-Sorted Signatures

(15)

Operational Semantics (in Frame Stack Style) (1/2)

hx:=e es,env,fsi−→he x:= es,env,fsiif¬val(e) assignment hi x:= es,env,fsi−→hx:=i es,env,fsi

hx:=i es,env,fsi−→hes,update(env,x,i),fsi

hx es,env,fsi−→hlookup(x,env) es,env,fsi identifier lookup he1+e2 es,env,fsi−→he1 +e2 es,env,fsiif¬val(e1) binary hi1 +e2 es,env,fsi−→hi1+e2 es,env,fsi operations hi1+e2 es,env,fsi−→he2 i1+ es,env,fsiif¬val(e2)

hi2 i1+ es,env,fsi−→hi1+i2 es,env,fsi hi1+i2 es,env,fsi−→hi1+i2 es,env,fsi

hnote es,env,fsi−→he not es,env,fsiif¬val(e) unary hb not es,env,fsi−→hnotb es,env,fsi operations hnotb es,env,fsi−→hb es,env,fsi

hif>thene2elsee3 es,env,fsi−→he2 es,env,fsi if-then-else hif⊥thene2elsee3 es,env,fsi−→he3 es,env,fsi

hife1thene2elsee3 es,env,fsi−→he1 ifthene2elsee3 es,env,fsi if¬val(e1) hb ifthene2elsee3 es,env,fsi−→hifbthene2elsee3 es,env,fsi hwhilee1doe2 es,env,fsi−→ while loop

hife1then(e2; whilee1doe2)else skip es,env,fsi

he1;e2 es,env,fsi−→he1 e2 es,env,fsi sequence hskip es,env,fsi−→hes,env,fsi skip

(16)

Operational Semantics (in Frame Stack Style) (2/2)

hcallf es,env,fsi−→hlookup(f,fs) es,env,fsi function calls hcallf(e) es,env,fsi−→hcallf call(e) es,env,fsi

hλx.fb call(e) es,env,fsi−→hcallλx.fb(e) es,env,fsi

hcallλx.fb(e) es,env,fsi−→he callλx.fb() es,env,fsiif¬val(e)

hi callλx.fb() es,env,fsi−→hcallλx.fb(i) es,env,fsi

hcallλx.fb(i) es,env,fsi−→hsubst(x,i,fb) es,env,fsi

(17)

Example Execution

h[x:=x+2],env,fsi −→

h[x+2,x:=],env,fsi −→ h[x,+2,x:=],env,fsi −→ h[12,+2,x:=],env,fsi −→ h[12+2,x:=],env,fsi −→ h[14,x:=],env,fsi −→ h[x:=14],env,fsi −→

h[],update(env,x,14),fsi 6−→.

(18)

Example Execution

h[x+2,x:=],env,fsi −→

h[x,+2,x:=],env,fsi −→ h[12,+2,x:=],env,fsi −→ h[12+2,x:=],env,fsi −→ h[14,x:=],env,fsi −→ h[x:=14],env,fsi −→

(19)

Example Execution

h[x,+2,x:=],env,fsi −→

h[12,+2,x:=],env,fsi −→ h[12+2,x:=],env,fsi −→ h[14,x:=],env,fsi −→ h[x:=14],env,fsi −→

(20)

Example Execution

h[12,+2,x:=],env,fsi −→

h[12+2,x:=],env,fsi −→ h[14,x:=],env,fsi −→ h[x:=14],env,fsi −→

(21)

Example Execution

h[12,+2,x:=],env,fsi −→

h[12+2,x:=],env,fsi −→

h[14,x:=],env,fsi −→ h[x:=14],env,fsi −→

(22)

Example Execution

h[12,+2,x:=],env,fsi −→

h[12+2,x:=],env,fsi −→

h[14,x:=],env,fsi −→

h[x:=14],env,fsi −→

(23)

Example Execution

h[12,+2,x:=],env,fsi −→

h[12+2,x:=],env,fsi −→

(24)

Example Execution

h[12,+2,x:=],env,fsi −→

h[12+2,x:=],env,fsi −→

(25)

Outline

1 Motivation

5 Application

6 Discussion

(26)

Defining Program Equivalence. The Case for Base Cases

A difficulty in defining program equivalence in a language parametric setting is that different languages may store theoutput(the result) in different places:

h[s:=f(5) + 2],env,fsi−→ ..

.

h[],update(env,s,42),fsi6−→.

hlet x = f(5) in x + 2i−→ ..

. 426−→.

We parametrize in the set of base case: we letBbe pairs of terminal configurations that are considered equivalent.

(27)

Defining Program Equivalence. The Case for Base Cases

h[s:=f(5) + 2],env,fsi−→

.. .

hlet x = f(5) in x + 2i−→

.. . 426−→.

(28)

Defining Program Equivalence. The Case for Base Cases

h[s:=f(5) + 2],env,fsi−→

.. .

hlet x = f(5) in x + 2i−→

.. . 426−→.

(29)

Simulations between Program Configurations

Given: Two operational semanticsRL andRR; the sorts CfgL and CfgR.

Definition (Full (Partial) Simulation)

A symbolic program configurationP is fully (partially) simulated by a symbolic program configuration Q under constraintφwith a set of base casesB, written

BP≺Qifφ (BPQifφ),

if, for any valuationρsuch thatρ(φ) =>and for any complete pathρ(P)−→^∗R_LP⁰, there exists a complete pathρ(Q)−→^∗R_R Q⁰ such that (P⁰,Q⁰)∈B(or – for partial simulation only – there exists an infinite pathρ(Q)−→R_R . . .);

(30)

Program Equivalence

Definition (Full (Partial) Equivalence)

Two symbolic program configurationsPandQ arefully equivalent (partially equivalent) under constraintφwith a set of base casesB, written

BP∼Qifφ (BP'Qifφ),

ifBP≺QifφandB⁻¹Q≺Pifφ(BPQifφandB⁻¹QPifφ).

(31)

Outline

1 Motivation

5 Application

6 Discussion

(32)

Basic Idea

We prove equivalence by two-sided simulation.

To proveP^≺..Q ifφ, we construct a set G of goals such that:

1 P^≺..Qifφ∈G;

2 G may contain other helper goals (lemmas). We provide a sound proof system:

Theorem (Soundness for full/partial simulation)

If G,B`⁰G andJBK⊆B, then for any simulation formula P^≺..Qifφ∈G, we have that

BP^≺..Qifφ.

(33)

Basic Idea

1 P^≺..Qifφ∈G;

2 G may contain other helper goals (lemmas).

We provide a sound proof system:

If G,B`⁰G andJBK⊆B, then for any simulation formula P^≺..Qifφ∈G, we have that

BP^≺..Qifφ.

(34)

Basic Idea

1 P^≺..Qifφ∈G;

2 G may contain other helper goals (lemmas).

We provide a sound proof system:

If G,B `⁰G andJBK⊆B, then for any simulation formula P^≺..Qifφ∈G, we have that

BP^≺..Qifφ.

(35)

Proof System for Simulation

Notation: sub

(P,Q),R ,W

P⁰≺..Q⁰ifφ⁰∈R∃var(P⁰,Q⁰, φ⁰).(φ⁰∧P=P⁰∧Q=Q⁰) Axiom

G,B`^gP^≺..Qif⊥ Base

G,B`^gP^≺..Qifφ∧ ¬φB

G,B`^g P^≺..Qifφ ^φ^B^→ W

Q⁰ifφ⁰∈∆^≤k_R

R(Q) φ⁰→sub

(P,Q⁰),B

Circ^≺

G,B`¹P≺Qifφ∧ ¬φG

G,B `¹P≺Qifφ ^φ^G^→ W

Q⁰ifφ⁰∈∆^≤k_R

R(Q) φ⁰→sub

(P,Q⁰),G

Circ

G,B`^g PQifφ∧ ¬φG

G,B`^gPQifφ ^φ^G^→ W

Q⁰ifφ⁰∈∆^{≥1−g,≤k}_R

R (Q)

φ⁰→sub

(P,Q⁰),G

Step

G,B`¹Pⁱ^≺..Qifφⁱ (for all 1≤i≤n) G,B`^g P^≺..Qifφ∧ ¬φ¹∧. . .∧ ¬φⁿ

G,B`^g P^≺..Qifφ ^∆^R^L^(P^if^φ)={P

i ifφⁱ|1≤i≤n}

(36)

Outline

1 Motivation

5 Application

(37)

Setting Resource Bounds

Let us assume that we are interested in interpretingWHprograms on a finite-stack machine.

Initial rewrite rule:

hx:=e es,env,fsi−→he x:= es,env,fsiif¬val(e) Updated rewrite rule:

hx:=e es,env,fsi−→he x:= es,env,fsiif¬val(e)∧len(es)<k

| {z }

new constraint

Call the initial languageWH1and the finite-stack languageWH2.

(38)

Setting Resource Bounds

hx:=e es,env,fsi−→he x:= es,env,fsiif¬val(e)

Updated rewrite rule:

| {z }

new constraint

(39)

Setting Resource Bounds

| {z }

new constraint

(40)

Setting Resource Bounds

| {z }

new constraint

(41)

Equivalence in the Presence of Resource Bounds

We study using our method the equivalence inWH1andWH2of the programs:

h[call f(N)],env,fsi and h[call F(N,0,0)],env,fsi

forN≥0, where the recursive functionsf andFare defined by the function map fs={f 7→λn.if n = 0 then 0 else n+call f(n−1),

F7→λn.λi.λa.if i≤n then call F(n,i+1,a+i) else a}.

(42)

The functions f and F

exp.

phase











h[f(3)]i −→^∗

h[f(2),3+]i −→^∗ h[f(1),2+,3+]i −→^∗ h[f(0),1+,2+,3+]i −→^∗ contr.

phase











h[0,1+,2+,3+]i −→^∗ h[1,2+,3+]i −→^∗ h[3,3+]i −→^∗

h[6]i 6−→

h[F(3,0,0)]i −→^∗ h[F(3,1,0)]i −→^∗ h[F(3,2,1)]i −→^∗ h[F(3,3,3)]i −→^∗ h[F(3,4,6)]i −→^∗ h[6]i 6−→

(43)

Equivalence in the Presence of Resource Bounds

We letB={(h[i],env,fsi,h[i⁰],env⁰,fs⁰i)|i=i⁰∧i,i⁰∈Z}.

G ={

h[call f(N)],env,fsi ^≺.. h[call F(N,0,0)],env,fsi if 0≤N, hcall f(I−1) reduce(I,N),env,fsi ^≺.. h[call F(N,0,0)],env,fsi if 0≤I≤N, hS reduce(I,N),env,fsi ^≺.. h[call F(N,I,S)],env,fsi if 1≤I≤N}, where

reduce(i,n)−→[] ifi>n,

reduce(i,n)−→(i+) reduce(i+1,n) if i≤n. Using the setsG,B defined above, we have that

G,B`⁰G for partial and full simulation and that

G⁻¹,B⁻¹`⁰G⁻¹ for partial simulation. Our proof system cannot showG⁻¹,B⁻¹`⁰G⁻¹for technical reasons.

So we prove partial equivalence betweenf andF, but only part of the full equivalence betweenf andF.

(44)

Equivalence in the Presence of Resource Bounds

G={

reduce(i,n)−→(i+) reduce(i+1,n) if i≤n.

Using the setsG,B defined above, we have that

G⁻¹,B⁻¹`⁰G⁻¹ for partial simulation. Our proof system cannot showG⁻¹,B⁻¹`⁰G⁻¹for technical reasons.

(45)

Equivalence in the Presence of Resource Bounds

G={

G⁻¹,B⁻¹`⁰G⁻¹ for partial simulation.

Our proof system cannot showG⁻¹,B⁻¹`⁰G⁻¹for technical reasons.

(46)

Equivalence in the Presence of Resource Bounds

G={

G⁻¹,B⁻¹`⁰G⁻¹ for partial simulation.

(47)

Outline

1 Motivation

5 Application

6 Discussion

(48)

Implementation

Prototype implementation of the two proof systems in theRMTtool at:

http://profs.info.uaic.ro/~stefan.ciobaca/wpte2021.

Example Ctrl RMT

fib02 4.02s 25.73s

fib03 3.06s 27.55s

fib04 Timeout 77.40s

fib05 3.99s 36.67s

fib06 32.81s 63.39s

fib07 2.74s 59.31s

fib08 3.44s 60.77s

fib09 3.09s 41.51s

fib10 2.34s 35.91s

fib11 Timeout 79.52s

fib12 No No

sum01 2.39s 10.51s

sum02 2.33s 12.36s

sum03 2.62s 12.30s

Optimization PEC CORK RMT

Code hoisting X 0.32s 0.41s

Constant propagation X 0.33s 0.31s

Copy propagation X 0.33s 0.26s

If-conversion X 0.34s 0.48s

Partial redundancy elimination X 0.34s 0.75s

Loop invariant code motion X 3.48s 3.79s

Loop peeling X 3.26s 0.97s

Loop unrolling X 12.17s 7.09s

Loop unswitching X 8.19s 4.71s

Software pipelining X 8.02s 3.56s

Loop fission X 23.45s ∗ 10.40s

Loop fusion X 23.34s ∗ 9.67s

Loop interchange X 29.30s ∗ 108.63s

Loop reversal X 8.41s 2.70s

Loop skewing X 8.50s 7.68s

Loop flattening × × ∗ 8.14s

(49)

Conclusion

1 Promising approach to operationally-based equivalence.

2 Requires extending LCTRSs withaxiomatized symbols(likereduce), which raise new research questions (unification modulo axiomatized symbols).

3 Our approach allows for nondeterminism in the definitions and proofs of equivalence, and we will exploit this in future work.

Thank you!