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