442 lines
16 KiB
Markdown
442 lines
16 KiB
Markdown
file:: [sle23-paper95_1682888032661_0.pdf](../assets/sle23-paper95_1682888032661_0.pdf)
|
||
file-path:: ../assets/sle23-paper95_1682888032661_0.pdf
|
||
|
||
- approach to define an executable semantics targeting the development of optimizing compilers.
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed678-8c79-42a6-a523-2cea2d8ef419
|
||
- ype checks
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed708-429c-49c9-95d3-39140d8b08f2
|
||
- primitive
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed70b-5f81-4cf4-998e-8b60e9879bf1
|
||
- alues boxing and unboxing
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed70f-1d40-476a-8baf-2c841cf958ab
|
||
- function calls
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed716-2eb6-4108-8d99-95474df37342
|
||
- semPy, a partial evaluator of our executable semantics
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed738-190c-4729-b578-00c935ec543c
|
||
- On some tasks, Zipi displays performance competitive with that of state of art Python implementations
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed74b-53ad-44c3-ae5e-2f1801a6b0d3
|
||
- While the syntax is formally specified, this is not the case of the semantics, leaving room for ambiguities and making it difficult to reason about Python
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed772-c110-49c2-af3b-7cc5df1a8792
|
||
- CPython, the reference implementation
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed797-342f-4736-9ef3-7c4e3b5db4b6
|
||
- RPython experiment
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed7b1-91e2-4842-b8d9-938da5e84915
|
||
- development of an executable semantics, written in the Python syntax, that aims to automate part of the implementation of a Python optimizing compiler.
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed7c1-2f39-45db-a99c-a11a463fb4ad
|
||
- overview of Python’s semantics
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed7e1-a4e8-4625-ba5e-e78640abda1d
|
||
- executable semantics that describes the behavior of various Python operations.
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed7e8-7ea9-4d0f-b32c-8443ce2bfd91
|
||
- technique for partial evaluation of our executable semantics that focuses on removing redundant type checks, boxing and unboxing, and method lookups and invocations from Python operations.
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed7f3-c2b3-4d30-8662-a0250b933bb8
|
||
- we show how we reused our executable semantics in the implementation of Zipi
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 644ed82f-68ac-4a06-8ea0-4e18cffa3bf6
|
||
- Python’s semantics is highly dynamic
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed8b2-7141-4433-9de8-8d2fed9350a6
|
||
- Python does not have an official formal semantics.
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed8bd-bf6e-43e7-9224-6441ca9d6a37
|
||
- we refer to the behavior of CPython
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: purple
|
||
id:: 644ed8ce-3fff-49a1-8e5c-d211c1596856
|
||
- identity
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644edbe1-425d-4f9f-953f-70a1eee826c5
|
||
- value
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644edbe4-8fcb-46c2-8f5f-d6b37e62d9bf
|
||
- type determines the operations allowed on the object.
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644edc32-9694-427c-b824-203f2500c993
|
||
- However, this is not possible for objects whose type is a built-in type such as booleans, floats, integers, strings, lists, tuples, sets and dictionaries
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644edc47-bfd5-47d1-9615-9d964a0fc4eb
|
||
- All values in a Python program are objects.
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644edc50-0c11-42fa-a519-2c0a86cb13c7
|
||
- The expression type(x).__add__ first looks for __add__ on type(x) itself. If no such method is found, it is looked up recursively on the parents of type(x)
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fdde3-026c-4d9e-8491-9287b192d97e
|
||
- method resolution order (MRO
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fddef-928d-4d60-889a-275563a5e3b0
|
||
- The values of their attributes may be updated, new attributes may be introduced, or existing ones may be removed
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fde76-2be1-4d63-8c9f-6b38110e595d
|
||
- An important exception is that attributes of all built-in types are read-only
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fde84-dc3e-4011-bcb4-53ed1ec50971
|
||
- Immutability of built-in types is part of Python’s semantics.
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fde97-7df2-4cd3-be39-61207bf1012b
|
||
- Python incorporates features such as dynamic typing, dynamic binding, and dynamic code evaluation.
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644fdfa2-cf9f-4cf7-8a6c-3c18dfcfca98
|
||
- Python supports modular programming through module objects
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe2a1-785f-467f-a592-d08d056273f8
|
||
- any modifications applied to a module’s attributes is reflected on its global environment.
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe2b7-09a9-4c4d-9acd-b237e76f9e6e
|
||
- An operation as simple as subtracting an integer and a floating point number requires two method searches in the MRO of int and float respectively
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe32c-2c30-4f7b-a62b-6e740481f75a
|
||
- This procedure, known as boxing and unboxing, leads to additional overhead [5]
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe360-695a-4a9b-8f4f-44a1e790e943
|
||
- xecutable semantics aimed at developing optimizing Python compilers
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe36e-583b-4982-b50a-3efa431d3d0b
|
||
- 1) automate the implementation of a [[PYTHON]] compiler,
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: yellow
|
||
id:: 644fe378-f02f-4626-bb6b-1b797d6c12b3
|
||
hl-stamp:: 1682957179733
|
||
- be easily reusable [[by]] existing [[PYTHON]] compilers
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: green
|
||
id:: 644fe3a1-93fb-427e-aec2-147425967c89
|
||
hl-stamp:: 1682957221312
|
||
- yield performant implementations
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: yellow
|
||
id:: 644fe3ad-606d-4a0f-b985-8134947edfcd
|
||
hl-stamp:: 1682957231924
|
||
- RPython
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: yellow
|
||
id:: 644fe5dc-a608-41ec-90ac-479206bfdf0c
|
||
- It differs in that we instead
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: yellow
|
||
id:: 644fe60f-0f34-42c5-a2bc-2cb6ac4060f0
|
||
- compiler intrinsics statement
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: yellow
|
||
id:: 644fe635-ccc4-4ded-9720-af2852297010
|
||
- Intrinsics imported with the compiler intrinsics statement are static, they cannot be shadowed [[by]] another assignment or assigned to a variab
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 644fe6e2-b255-472c-ae84-a88032fe6835
|
||
hl-stamp:: 1682958056044
|
||
- addition
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 644fe729-e3a8-4f0b-a916-b478f3a6370f
|
||
- These examples effectively illustrate why seemingly simple operations incur a significant overhead.
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 644fe73b-7ce7-4159-8c24-735bba4f43be
|
||
- [:span]
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: green
|
||
id:: 644feb0a-3015-4266-907b-40e6abd43436
|
||
hl-type:: area
|
||
hl-stamp:: 1682959114081
|
||
- class_getattr
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 6450131f-fb3a-445f-a406-c06df5147bea
|
||
- absent
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 64501321-fece-4916-90c2-f9dd0f7cb56c
|
||
- normal
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 64501669-7f6e-4d90-852a-4f0f2b0f3cc0
|
||
- reflected
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 6450166b-efb7-48b3-9fcd-91e1c789d9b1
|
||
- a semantics
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 64501688-27cb-46fb-8e64-bb7d280a6b77
|
||
- semantics of
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 6450168b-d80b-4701-a50a-b0981968b34b
|
||
- This allows us to define the notion of behavior, a specialization of an operator for a given combination of built-in types.
|
||
ls-type:: annotation
|
||
hl-page:: 12
|
||
hl-color:: green
|
||
id:: 64501799-4f47-4d73-af89-3a736156bf15
|
||
- Zipi compiles behaviors and dispatches operations to their corresponding behaviors at run time.
|
||
ls-type:: annotation
|
||
hl-page:: 12
|
||
hl-color:: purple
|
||
id:: 645017bf-849d-4665-a879-91a3aa34ab76
|
||
- PyPy
|
||
ls-type:: annotation
|
||
hl-page:: 12
|
||
hl-color:: yellow
|
||
id:: 645017c6-757f-40a8-8461-4f7fb63479dd
|
||
- It appears to us that they would be well suited for CPython, as they specifically address the known overhead of this implementation
|
||
ls-type:: annotation
|
||
hl-page:: 12
|
||
hl-color:: green
|
||
id:: 645017ec-07e4-4eb9-a940-cb54f7c71008
|
||
- This section presents semPy3, a Python tool for generating behaviors by removing redundant type checks, boxing and unboxing, and method calls whenever possible
|
||
ls-type:: annotation
|
||
hl-page:: 7
|
||
hl-color:: green
|
||
id:: 64501b49-37e7-43f6-a9a8-6cd9548c5831
|
||
- semPy is a Python partial evaluator supporting the compiler intrinsics statement.
|
||
ls-type:: annotation
|
||
hl-page:: 7
|
||
hl-color:: yellow
|
||
id:: 64501b57-a394-4c43-9dd4-f302dd17c5d3
|
||
- It outputs a specialization of the semantics given that context, which is a behavior.
|
||
ls-type:: annotation
|
||
hl-page:: 7
|
||
hl-color:: purple
|
||
id:: 64501b77-d4f6-400a-869d-8c88ca84fe5b
|
||
- add_intX_floatY was generated from the add semantics (Figure 3) in a context where the left-hand operand is an int and the right-hand operand is a float
|
||
ls-type:: annotation
|
||
hl-page:: 7
|
||
hl-color:: blue
|
||
id:: 64501b97-fc3f-4ea7-ac34-bec5ce768cb9
|
||
hl-stamp:: 1682971545826
|
||
- we configured our benchmarks to only measure the run time performance of the program after initialization
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: green
|
||
id:: 6451854d-ddd6-4638-b46a-065d44249997
|
||
- or
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: red
|
||
id:: 6451856b-a483-4390-8b4a-5a1513822cd2
|
||
- operations suffering from poor performance.
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: green
|
||
id:: 645185b1-4388-4327-b89f-dc3b7c9c9f50
|
||
- The operation being evaluated is wrapped in a loop to reach a measurable time on the order of one second on CPython.
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: green
|
||
id:: 645185be-c478-4062-b66d-62a1b30f8623
|
||
- uncompetitive in comparison to static languages such as C
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: green
|
||
id:: 6452262b-c2a5-45e9-936e-b1c6aafb4a04
|
||
- The effort spent getting the semantics right leaves little [[time]] for optimization
|
||
ls-type:: annotation
|
||
hl-page:: 1
|
||
hl-color:: blue
|
||
id:: 645228f1-38c2-4ae0-b579-823a46cf2b28
|
||
hl-stamp:: 1683106035825
|
||
- methods governing operations are called magic methods.
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: purple
|
||
id:: 64522a40-df2b-40c5-ac97-11a12e2612b1
|
||
hl-stamp:: 1683106371076
|
||
- The only operators that cannot be overloaded are the “is” operator which compares objects by identity, and the “and”,“or” and “not” boolean operators
|
||
ls-type:: annotation
|
||
hl-page:: 2
|
||
hl-color:: purple
|
||
id:: 64522aaa-e11f-43f2-b5de-ee3550d58fea
|
||
- automate this process to accelerate development, including that of existing compilers, independently of the language and tools chosen for its implementation.
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: purple
|
||
id:: 64522e0a-730b-4302-97c2-cb1bd4b3acca
|
||
- interface with the semantics by using the parsing infrastructure of an existing compiler.
|
||
ls-type:: annotation
|
||
hl-page:: 3
|
||
hl-color:: yellow
|
||
id:: 64522e83-2ecd-4c6a-bacf-e604cfeb447d
|
||
hl-stamp:: 1683107462697
|
||
- optimized versions of various operators in sections 5 and
|
||
ls-type:: annotation
|
||
hl-page:: 4
|
||
hl-color:: green
|
||
id:: 64522ec4-6715-4632-9a37-71aef6cd8a67
|
||
hl-stamp:: 1683107527781
|
||
- Behaviors
|
||
ls-type:: annotation
|
||
hl-page:: 6
|
||
hl-color:: green
|
||
id:: 645232f1-27ff-4c60-a8aa-e9ad76f7eff9
|
||
- A compiler can implement arithmetic operators from the semantics defined in Section 3. Yet, by doing so in a naive way, that is calling each magic method, the implementation would likely offer poor performance.
|
||
ls-type:: annotation
|
||
hl-page:: 6
|
||
hl-color:: green
|
||
id:: 6452331a-4d1a-48c4-b3d9-7c0e01558c82
|
||
- We exploit that fact to generate optimized versions of Python operators.
|
||
ls-type:: annotation
|
||
hl-page:: 6
|
||
hl-color:: green
|
||
id:: 64523401-621a-4d9c-af49-0bbc838d177b
|
||
- When a semantics or magic method is invoked, semPy systematically inlines the callee’s [[code]] at the [[CALL]] site. This removes magic method calls from semantics specializations. Magic methods are returned by invocations of the class_getattr intrinsic function. This function is always called on the arguments of a semantics, whose types are provided in the type context, so it is always possible to resolve which magic method is to be called, or if that method is absent.
|
||
ls-type:: annotation
|
||
hl-page:: 7
|
||
hl-color:: yellow
|
||
id:: 645270f9-9991-40aa-b8cf-42d909fc85fd
|
||
hl-stamp:: 1683124476488
|
||
- optimizing [[PYTHON]] compiler.
|
||
ls-type:: annotation
|
||
hl-page:: 9
|
||
hl-color:: purple
|
||
id:: 64527140-4f7d-40d0-a58c-4db765477243
|
||
hl-stamp:: 1683124552273
|
||
- Zipi compiles [[PYTHON]] to Scheme [[code]], which is then compiled to an executable using either the Bigloo [7] or Gambit [8] Scheme compilers
|
||
ls-type:: annotation
|
||
hl-page:: 9
|
||
hl-color:: yellow
|
||
id:: 64527182-5134-4f53-9126-eb3069193e4f
|
||
hl-stamp:: 1683124613750
|
||
- Performance was measured through microbenchmarks as well as regular benchmarks implementing well-known algorithms
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452738f-a8b3-42c8-bbe8-6887ded91ba9
|
||
- Zipi has a significant compilation overhead because it is AOT and has a deep pipeline that compiles Python code to Scheme, then to C, and finally to machine code.
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 645273a0-f0c0-4759-ae0d-d9717fe0babb
|
||
- Benchmarks measure real time using the Python time module which all implementations provide.
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452ba2e-27ba-45bc-bb08-c97e83fa8d55
|
||
- To minimize the loop overhead, its body contains several repetitions of the measured operation (typically 20
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452bd0c-bde8-477e-b00a-7e3b2747b09f
|
||
- Unfortunately, it does not allow a comparison with PyPy which treats the kernel of many of our benchmarks as dead cod
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452bd82-bae0-4c14-b0e2-c8a13a6dd9db
|
||
- Performance improvements from other optimizations unrelated to behaviors also show up in the microbenchmarks
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452bec7-50a0-4330-b516-8e8d2dd905db
|
||
- For instance, assignment to global variables, function calls and iteration on built-in types are all faster than with CPython
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452becd-3128-4dd1-a6df-c0913f0e70cc
|
||
- On the other hand, some microbenchmarks display poor performance. Those are unoptimized features that we implemented in a naive way, such as function calls with keyword arguments.
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452bed2-863a-4a94-becb-c70fe197dbb3
|
||
- Zipi being at an early development stage, only four benchmarks from PyPerformance are supported at the moment, hence the need for custom benchmarks
|
||
ls-type:: annotation
|
||
hl-page:: 11
|
||
hl-color:: yellow
|
||
id:: 6452beee-2cf9-4990-b595-620cd469b4e5
|
||
- We wish to extend the behavior optimization to other operations in the future to further analyze its impact on performance
|
||
ls-type:: annotation
|
||
hl-page:: 12
|
||
hl-color:: yellow
|
||
id:: 6452bf9c-18e8-4d21-99ea-58199131bde6 |