Logical Relations in Programming Languages

Explore the concept of logical relations in programming languages, focusing on the relation between high-level and low-level programs. Learn about contextual equivalence, its benefits and limitations, and how logical relations offer a robust framework for defining program equivalence. Discover why logical relations are preferred over other techniques and how they enable compositionality and extensionality in proving equivalence.

• Programming Languages
• Logical Relations
• Contextual Equivalence
• Equivalence Definition

dwia337 Follow

Uploaded on Sep 11, 2024 | 1 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

Presentation Transcript

1. A Kripke Logical Relation Between ML and Assembly Chung-Kil Hur and Derek Dreyer MPI-SWS POPL 2011

2. Compiler Correctness by Simulation Relation execution compiler Read Read Write Write Send Send

3. Limitation of Simulation Relation: Lack of Compositionality compiler1 compiler2 ? ?

4. Essential Question When is a high-level program equivalent to a low-level program? Want a notion of program equivalence that is 1. preserved under linking 2. as large as possible

5. What is Contextual Equivalence? Canonical notion of program equivalence for high-level programs: ?1 ctx?2 C[?1] and C[?2] return the same observable results for every program context C

6. What is good about Contextual Equivalence? Compositionality: ?1 ctxf2 S T ( ?1?2. ?1 ctx?2 S ?1?1 ctx?2?2 T) Extensionality: ?1?2. ?1 ctx?2 S ?1?1 ctx?2?2 T ?1 ctx?2 S T

7. What is wrong with Contextual Equivalence? But: Does not work for low-level languages Contexts have too much distinguishing power Does not work for relating different languages Can t use same context for two different languages

8. Logical Relations to the Rescue! [Benton & Hur, ICFP 09] Typically used as technique for proving contextual equivalence in a higher-order language ?2 ?1 log S T ?2?2 T ?1?2. ?1 log S ?1?1 log ?2 Take logical relation as definition of program equivalence between high-level and low-level languages

9. Why is Logical Relation a good definition? ?2 ?2 ?1 log S T ?1?2. ?1 log S ?1?1 log ?2?2 T ?2 ?2 apply(?2,?2) T ?2?2 T Compositionality and extensionality are built in! Unlike ctx , logical relations can be adapted to relate different languages. ICFP 09 paper related pure ?-calculus and SECD

10. Contributions of This Work Scale ideas to ML-like high-level language and assembly-like low-level language Builds on recent work on step-indexed Kripke logical relations (by Dreyer et al. POPL 09, ICFP 10) Handle interaction with a garbage collector Distinguish between logical and physical memories (idea from McCreight et al. PLDI 07, ICFP 10)

11. Kripke Logical Relations Relating ML to assembly is challenging Need a way to tame state, at both high and low levels Kripke logical relations are logical relations indexed by possible worlds Worlds encode invariants about state Dreyer et al. [ICFP 10] generalize worlds to express state transition systems Supports reasoning about how state evolves over time

12. Irreversible State Change[Dreyer et al.] e1= f:???? ????.(f ;1) e2= ??? x = ??? 0 ?? f:???? ????. x 1;f ; !x ? 0 ? 1? (can be in either state) (no successor)

13. Self-Modifying Code e1= f:???? ????.(f ;1) bg move wk4 bg+3 move wk5 1 jmp alloc move [wk5+0]h bg+5 jmp wk0 bg+5 bg+13 1 move wk3 bg+10 isr wk4 wk3 minus wk4 wk4 666 isw wk3 wk4 plus wk3 wk3 1 (jneq bg+6 (isw bg+5 bg+12 (move [wk1+0]h bg+13 bg+13 (plus sp (move [sp-1]s wk0 (move wk1 wk2 (move wk0 bg+18 (jmp [wk1+0]h (move wk5 1 (minus sp (jmp [sp-0]s )+666 01100010001000111100111100111011 jmp [sp-0]s bg+5 jmp bg+12 bg+5 bg+13 2 01100110010101001110110001101011 01101010101101110101000100100101 bg+12 10110101001111010101010111000100 bg+13 01010110101001010101110110001010 11011001010111000101010101001010 11010101000101011010010101010101 01110110100101011100101010100101 10101010100100110110001000111010 10010001000011101111001111001010 01110100010010101010010101010010 minus sp wk3 (jmp bg+12) )+666 (jmp bg+12) bg+21)+666 bg+21 jneq bg+6 isw bg+5 wk3 bg+5 3 bg+12 move [wk1+0]h bg+13 bg+13 plus sp move [sp-1]s wk0 move wk1 wk2 move wk0 bg+18 jmp [wk1+0]h move wk5 1 )+666 )+666 )+666 )+666 )+666 )+666 )+666 )+666 sp 1 sp 1 sp 1 sp 1

14. Reasoning about Self-Modifying Code (CASE 2) (CASE 1) (CASE 3) e1= f:???? ????.(f ;1) bg move wk4 bg+3 move wk5 1 jmp alloc move [wk5+0]h bg+5 jmp wk0 decrypted bg + 5 decrypted encrypted decrypted bg + 13 encrypted bg + 5 encrypted bg + 13 bg + 13 bg + 5 move wk3 bg+10 isr wk4 wk3 minus wk4 wk4 666 isw wk3 wk4 plus wk3 wk3 1 01100110010101001110110001101011 01101010101101110101000100100101 bg+12 10110101001111010101010111000100 bg+13 01010110101001010101110110001010 11011001010111000101010101001010 11010101000101011010010101010101 01110110100101011100101010100101 10101010100100110110001000111010 10010001000011101111001111001010 01110100010010101010010101010010 01100010001000111100111100111011 jmp [sp-0]s bg+5 jmp bg+12 jneq bg+6 isw bg+5 wk3 (jmp bg+12) bg+21 bg+12 move [wk1+0]h bg+13 bg+13 plus sp move [sp-1]s wk0 move wk1 wk2 move wk0 bg+18 jmp [wk1+0]h move wk5 1 minus sp sp 1 bg+5 bg+13 sp 1

15. What Else is in the Paper? Public vs. private transitions Idea from Dreyer et al., useful for modeling well-bracketed state change, e.g. assumptions about stack & callee-save registers Logical vs. physical memories Idea from McCreight et al., critical for defining logical relations that enjoy monotonicity property in the presence of GC Symmetric, language-generic presentation of logical relation Compiler correctness for simple compiler Full proofs in online appendix

16. Conclusion Progress toward a more general notion of equivalence between high- and low-level programs We ve generalized previous work to a much more realistic setting Applying cool new ideas from recent work on both logical relations and certified compilers

17. Future Work Compositional Compiler Correctness for C (Linking for CompCert) Realistic Compilation Multiphase Compilation

18. Future Work Linking between different languages ML C ML+C