Programming Journal, Volume '24: "A VM-Agnostic and Backwards ..."
A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages
Iona Thomas, Vincent Aranega, Stéphane Ducasse, Guillermo Polito, and Pablo Tesone
(University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9189 CRIStAL, France)
In object-oriented languages, method visibility modifiers hold a key role in separating internal methods from the public API. Protected visibility modifiers offer a way to hide methods from external objects while autho- rizing internal use and overriding in subclasses. While present in main statically-typed languages, visibility modifiers are not as common or mature in dynamically-typed languages. In this article, we present ProtDyn, a self-send-based visibility model calculated at compile time for dynamically- typed languages relying on name-mangling and syntactic differentiation of self vs non self sends. We present #Pharo, a ProtDyn implementation of this model that is backwards compatible with existing programs, and its port to Python. Using these implementations we study the performance impact of Prot- Dyn on the method lookup, in the presence of global lookup caches and polymorphic inline caches. We show that our name mangling and double method registration technique has a very low impact on performance and keeps the benefits from the global lookup cache and polymorphic inline cache. We also show that the memory overhead on a real use case is between 2% and 13% in the worst-case scenario. Protected modifier semantics enforces encapsulation such as private but allow developers to still extend the class in subclasses. ProtDyn offers a VM-agnostic and backwards-compatible design to introduce protected semantics in dynamically-typed languages.
@Article{Programming Journal, Volume24p2,
author = {Iona Thomas and Vincent Aranega and Stéphane Ducasse and Guillermo Polito and Pablo Tesone},
title = {A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages},
journal = {},
volume = {},
number = {},
articleno = {2},
numpages = {36},
doi = {10.22152/programming-journal.org/2024/8/2},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "McMini: A Programmable DPOR-Based ..."
McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs
Maxwell Pirtle, Luka Jovanovic, and Gene Cooperman
(Northeastern University, USA)
P@GrayFGContext Model checking has become a key tool for gaining confidence in correctness of multi-threaded programs. Unit tests and functional tests do not suffice because of race conditions that are not discovered by those tests. This problem is addressed by model checking tools. A simple model checker is useful for detecting race conditions prior to production.
P@GrayFGInquiry Current model checkers hardwire the behavior of common thread operations, and do not recognize application-dependent thread paradigms or functions using simpler primitive operations. This introduces additional operations, causing current model checkers to be excessively slow. In addition, there is no mechanism to model the semantics of the actual thread wakeup policies implemented in the underlying thread library or operating system. Eliminating these constraints can make model checkers faster.
P@GrayFGApproach McMini is an extensible model checker based on DPOR (Dynamic Partial Order Reduction). A mechanism was invented to declare to McMini new, primitive thread operations, typically in 100 lines or less of C code. The mechanism was extended to also allow a user of McMini to declare alternative thread wakeup policies, including spurious wakeups from condition variables.
P@GrayFGKnowledge In McMini, the user defines new thread operations. The user optimizes these operations by declaring to the DPOR algorithm information that reduces the number of thread schedules to be searched. One declares: (i) under what conditions an operation is enabled; (ii) which thread operations are independent of each other; and (iii) when two operations can be considered as co-enabled. An optional wakeup policy is implemented by defining when a wait operation (on a semaphore, condition variable, etc.) is enabled. A new enqueue thread operation is described, allowing a user to declare alternative wakeup policies.
P@GrayFGGrounding McMini was first confirmed to operate correctly and efficiently as a traditional, but extensible model checker for mutex, semaphore, condition variable, and reader-writer lock. McMini’s extensibility was then tested on novel primitive operations, representing other useful paradigms for multithreaded operations. An example is readers-and-two-writers. The speed of model checking was found to be five times faster and more, as compared to traditional implementations on top of condition variables. Alternative wakeup policies (e.g., FIFO, LIFO, arbitrary, etc.) were then tested using an enqueue operation. Finally, spurious wakeups were tested with a program that exposes a bug only in the presence of a spurious wakeup.
P@GrayFGImportance Many applications employ functions for multithreaded paradigms that go beyond the traditional mutex, semaphore, and condition variables. They are defined on top of basic operations. The ability to directly define new primitives for these paradigms makes model checkers run faster by searching fewer thread schedules. The ability to model particular thread wakeup policies, including spurious wakeup for condition variables, is also important. Note that POSIX leaves undefined the wakeup policies of pthread_mutex_lock, sem_wait, and pthread_cond_wait. The POSIX thread implementation then chooses a particular policy (e.g., FIFO, arbitrary), which can be directly modeled by McMini.
@Article{Programming Journal, Volume24p1,
author = {Maxwell Pirtle and Luka Jovanovic and Gene Cooperman},
title = {McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs},
journal = {},
volume = {},
number = {},
articleno = {1},
numpages = {32},
doi = {10.22152/programming-journal.org/2024/8/1},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "A VM-Agnostic and Backwards ..."
A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages
Iona Thomas, Vincent Aranega, Stéphane Ducasse, Guillermo Polito, and Pablo Tesone
(University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9189 CRIStAL, France)
In object-oriented languages, method visibility modifiers hold a key role in separating internal methods from the public API. Protected visibility modifiers offer a way to hide methods from external objects while autho- rizing internal use and overriding in subclasses. While present in main statically-typed languages, visibility modifiers are not as common or mature in dynamically-typed languages. In this article, we present ProtDyn, a self-send-based visibility model calculated at compile time for dynamically- typed languages relying on name-mangling and syntactic differentiation of self vs non self sends. We present #Pharo, a ProtDyn implementation of this model that is backwards compatible with existing programs, and its port to Python. Using these implementations we study the performance impact of Prot- Dyn on the method lookup, in the presence of global lookup caches and polymorphic inline caches. We show that our name mangling and double method registration technique has a very low impact on performance and keeps the benefits from the global lookup cache and polymorphic inline cache. We also show that the memory overhead on a real use case is between 2% and 13% in the worst-case scenario. Protected modifier semantics enforces encapsulation such as private but allow developers to still extend the class in subclasses. ProtDyn offers a VM-agnostic and backwards-compatible design to introduce protected semantics in dynamically-typed languages.
@Article{Programming Journal, Volume24p2,
author = {Iona Thomas and Vincent Aranega and Stéphane Ducasse and Guillermo Polito and Pablo Tesone},
title = {A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages},
journal = {},
volume = {},
number = {},
articleno = {2},
numpages = {36},
doi = {10.22152/programming-journal.org/2024/8/2},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "McMini: A Programmable DPOR-Based ..."
McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs
Maxwell Pirtle, Luka Jovanovic, and Gene Cooperman
(Northeastern University, USA)
P@GrayFGContext Model checking has become a key tool for gaining confidence in correctness of multi-threaded programs. Unit tests and functional tests do not suffice because of race conditions that are not discovered by those tests. This problem is addressed by model checking tools. A simple model checker is useful for detecting race conditions prior to production.
P@GrayFGInquiry Current model checkers hardwire the behavior of common thread operations, and do not recognize application-dependent thread paradigms or functions using simpler primitive operations. This introduces additional operations, causing current model checkers to be excessively slow. In addition, there is no mechanism to model the semantics of the actual thread wakeup policies implemented in the underlying thread library or operating system. Eliminating these constraints can make model checkers faster.
P@GrayFGApproach McMini is an extensible model checker based on DPOR (Dynamic Partial Order Reduction). A mechanism was invented to declare to McMini new, primitive thread operations, typically in 100 lines or less of C code. The mechanism was extended to also allow a user of McMini to declare alternative thread wakeup policies, including spurious wakeups from condition variables.
P@GrayFGKnowledge In McMini, the user defines new thread operations. The user optimizes these operations by declaring to the DPOR algorithm information that reduces the number of thread schedules to be searched. One declares: (i) under what conditions an operation is enabled; (ii) which thread operations are independent of each other; and (iii) when two operations can be considered as co-enabled. An optional wakeup policy is implemented by defining when a wait operation (on a semaphore, condition variable, etc.) is enabled. A new enqueue thread operation is described, allowing a user to declare alternative wakeup policies.
P@GrayFGGrounding McMini was first confirmed to operate correctly and efficiently as a traditional, but extensible model checker for mutex, semaphore, condition variable, and reader-writer lock. McMini’s extensibility was then tested on novel primitive operations, representing other useful paradigms for multithreaded operations. An example is readers-and-two-writers. The speed of model checking was found to be five times faster and more, as compared to traditional implementations on top of condition variables. Alternative wakeup policies (e.g., FIFO, LIFO, arbitrary, etc.) were then tested using an enqueue operation. Finally, spurious wakeups were tested with a program that exposes a bug only in the presence of a spurious wakeup.
P@GrayFGImportance Many applications employ functions for multithreaded paradigms that go beyond the traditional mutex, semaphore, and condition variables. They are defined on top of basic operations. The ability to directly define new primitives for these paradigms makes model checkers run faster by searching fewer thread schedules. The ability to model particular thread wakeup policies, including spurious wakeup for condition variables, is also important. Note that POSIX leaves undefined the wakeup policies of pthread_mutex_lock, sem_wait, and pthread_cond_wait. The POSIX thread implementation then chooses a particular policy (e.g., FIFO, arbitrary), which can be directly modeled by McMini.
@Article{Programming Journal, Volume24p1,
author = {Maxwell Pirtle and Luka Jovanovic and Gene Cooperman},
title = {McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs},
journal = {},
volume = {},
number = {},
articleno = {1},
numpages = {32},
doi = {10.22152/programming-journal.org/2024/8/1},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "Coqlex: Generating Formally ..."
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, and Lutz Strassburger
(Siemens Mobility, France; Inria, France; École Polytechnique, France)
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components.
However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability.
In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators.
The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices.
We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++.
Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends.
@Article{Programming Journal, Volume24p3,
author = {Wendlasida Ouedraogo and Gabriel Scherer and Lutz Strassburger},
title = {Coqlex: Generating Formally Verified Lexers},
journal = {},
volume = {},
number = {},
articleno = {3},
numpages = {30},
doi = {10.22152/programming-journal.org/2024/8/3},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "McMini: A Programmable DPOR-Based ..."
McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs
Maxwell Pirtle, Luka Jovanovic, and Gene Cooperman
(Northeastern University, USA)
P@GrayFGContext Model checking has become a key tool for gaining confidence in correctness of multi-threaded programs. Unit tests and functional tests do not suffice because of race conditions that are not discovered by those tests. This problem is addressed by model checking tools. A simple model checker is useful for detecting race conditions prior to production.
P@GrayFGInquiry Current model checkers hardwire the behavior of common thread operations, and do not recognize application-dependent thread paradigms or functions using simpler primitive operations. This introduces additional operations, causing current model checkers to be excessively slow. In addition, there is no mechanism to model the semantics of the actual thread wakeup policies implemented in the underlying thread library or operating system. Eliminating these constraints can make model checkers faster.
P@GrayFGApproach McMini is an extensible model checker based on DPOR (Dynamic Partial Order Reduction). A mechanism was invented to declare to McMini new, primitive thread operations, typically in 100 lines or less of C code. The mechanism was extended to also allow a user of McMini to declare alternative thread wakeup policies, including spurious wakeups from condition variables.
P@GrayFGKnowledge In McMini, the user defines new thread operations. The user optimizes these operations by declaring to the DPOR algorithm information that reduces the number of thread schedules to be searched. One declares: (i) under what conditions an operation is enabled; (ii) which thread operations are independent of each other; and (iii) when two operations can be considered as co-enabled. An optional wakeup policy is implemented by defining when a wait operation (on a semaphore, condition variable, etc.) is enabled. A new enqueue thread operation is described, allowing a user to declare alternative wakeup policies.
P@GrayFGGrounding McMini was first confirmed to operate correctly and efficiently as a traditional, but extensible model checker for mutex, semaphore, condition variable, and reader-writer lock. McMini’s extensibility was then tested on novel primitive operations, representing other useful paradigms for multithreaded operations. An example is readers-and-two-writers. The speed of model checking was found to be five times faster and more, as compared to traditional implementations on top of condition variables. Alternative wakeup policies (e.g., FIFO, LIFO, arbitrary, etc.) were then tested using an enqueue operation. Finally, spurious wakeups were tested with a program that exposes a bug only in the presence of a spurious wakeup.
P@GrayFGImportance Many applications employ functions for multithreaded paradigms that go beyond the traditional mutex, semaphore, and condition variables. They are defined on top of basic operations. The ability to directly define new primitives for these paradigms makes model checkers run faster by searching fewer thread schedules. The ability to model particular thread wakeup policies, including spurious wakeup for condition variables, is also important. Note that POSIX leaves undefined the wakeup policies of pthread_mutex_lock, sem_wait, and pthread_cond_wait. The POSIX thread implementation then chooses a particular policy (e.g., FIFO, arbitrary), which can be directly modeled by McMini.
@Article{Programming Journal, Volume24p1,
author = {Maxwell Pirtle and Luka Jovanovic and Gene Cooperman},
title = {McMini: A Programmable DPOR-Based Model Checker for Multithreaded Programs},
journal = {},
volume = {},
number = {},
articleno = {1},
numpages = {32},
doi = {10.22152/programming-journal.org/2024/8/1},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "A VM-Agnostic and Backwards ..."
A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages
Iona Thomas, Vincent Aranega, Stéphane Ducasse, Guillermo Polito, and Pablo Tesone
(University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9189 CRIStAL, France)
In object-oriented languages, method visibility modifiers hold a key role in separating internal methods from the public API. Protected visibility modifiers offer a way to hide methods from external objects while autho- rizing internal use and overriding in subclasses. While present in main statically-typed languages, visibility modifiers are not as common or mature in dynamically-typed languages. In this article, we present ProtDyn, a self-send-based visibility model calculated at compile time for dynamically- typed languages relying on name-mangling and syntactic differentiation of self vs non self sends. We present #Pharo, a ProtDyn implementation of this model that is backwards compatible with existing programs, and its port to Python. Using these implementations we study the performance impact of Prot- Dyn on the method lookup, in the presence of global lookup caches and polymorphic inline caches. We show that our name mangling and double method registration technique has a very low impact on performance and keeps the benefits from the global lookup cache and polymorphic inline cache. We also show that the memory overhead on a real use case is between 2% and 13% in the worst-case scenario. Protected modifier semantics enforces encapsulation such as private but allow developers to still extend the class in subclasses. ProtDyn offers a VM-agnostic and backwards-compatible design to introduce protected semantics in dynamically-typed languages.
@Article{Programming Journal, Volume24p2,
author = {Iona Thomas and Vincent Aranega and Stéphane Ducasse and Guillermo Polito and Pablo Tesone},
title = {A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages},
journal = {},
volume = {},
number = {},
articleno = {2},
numpages = {36},
doi = {10.22152/programming-journal.org/2024/8/2},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "Coqlex: Generating Formally ..."
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, and Lutz Strassburger
(Siemens Mobility, France; Inria, France; École Polytechnique, France)
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components.
However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability.
In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators.
The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices.
We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++.
Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends.
@Article{Programming Journal, Volume24p3,
author = {Wendlasida Ouedraogo and Gabriel Scherer and Lutz Strassburger},
title = {Coqlex: Generating Formally Verified Lexers},
journal = {},
volume = {},
number = {},
articleno = {3},
numpages = {30},
doi = {10.22152/programming-journal.org/2024/8/3},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "Coqlex: Generating Formally ..."
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, and Lutz Strassburger
(Siemens Mobility, France; Inria, France; École Polytechnique, France)
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components.
However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability.
In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators.
The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices.
We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++.
Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends.
@Article{Programming Journal, Volume24p3,
author = {Wendlasida Ouedraogo and Gabriel Scherer and Lutz Strassburger},
title = {Coqlex: Generating Formally Verified Lexers},
journal = {},
volume = {},
number = {},
articleno = {3},
numpages = {30},
doi = {10.22152/programming-journal.org/2024/8/3},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "A VM-Agnostic and Backwards ..."
A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages
Iona Thomas, Vincent Aranega, Stéphane Ducasse, Guillermo Polito, and Pablo Tesone
(University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9189 CRIStAL, France)
In object-oriented languages, method visibility modifiers hold a key role in separating internal methods from the public API. Protected visibility modifiers offer a way to hide methods from external objects while autho- rizing internal use and overriding in subclasses. While present in main statically-typed languages, visibility modifiers are not as common or mature in dynamically-typed languages. In this article, we present ProtDyn, a self-send-based visibility model calculated at compile time for dynamically- typed languages relying on name-mangling and syntactic differentiation of self vs non self sends. We present #Pharo, a ProtDyn implementation of this model that is backwards compatible with existing programs, and its port to Python. Using these implementations we study the performance impact of Prot- Dyn on the method lookup, in the presence of global lookup caches and polymorphic inline caches. We show that our name mangling and double method registration technique has a very low impact on performance and keeps the benefits from the global lookup cache and polymorphic inline cache. We also show that the memory overhead on a real use case is between 2% and 13% in the worst-case scenario. Protected modifier semantics enforces encapsulation such as private but allow developers to still extend the class in subclasses. ProtDyn offers a VM-agnostic and backwards-compatible design to introduce protected semantics in dynamically-typed languages.
@Article{Programming Journal, Volume24p2,
author = {Iona Thomas and Vincent Aranega and Stéphane Ducasse and Guillermo Polito and Pablo Tesone},
title = {A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages},
journal = {},
volume = {},
number = {},
articleno = {2},
numpages = {36},
doi = {10.22152/programming-journal.org/2024/8/2},
year = {2024},
}
Publisher's Version
Programming Journal, Volume '24: "A VM-Agnostic and Backwards ..."
A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages
Iona Thomas, Vincent Aranega, Stéphane Ducasse, Guillermo Polito, and Pablo Tesone
(University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9189 CRIStAL, France)
In object-oriented languages, method visibility modifiers hold a key role in separating internal methods from the public API. Protected visibility modifiers offer a way to hide methods from external objects while autho- rizing internal use and overriding in subclasses. While present in main statically-typed languages, visibility modifiers are not as common or mature in dynamically-typed languages. In this article, we present ProtDyn, a self-send-based visibility model calculated at compile time for dynamically- typed languages relying on name-mangling and syntactic differentiation of self vs non self sends. We present #Pharo, a ProtDyn implementation of this model that is backwards compatible with existing programs, and its port to Python. Using these implementations we study the performance impact of Prot- Dyn on the method lookup, in the presence of global lookup caches and polymorphic inline caches. We show that our name mangling and double method registration technique has a very low impact on performance and keeps the benefits from the global lookup cache and polymorphic inline cache. We also show that the memory overhead on a real use case is between 2% and 13% in the worst-case scenario. Protected modifier semantics enforces encapsulation such as private but allow developers to still extend the class in subclasses. ProtDyn offers a VM-agnostic and backwards-compatible design to introduce protected semantics in dynamically-typed languages.
@Article{Programming Journal, Volume24p2,
author = {Iona Thomas and Vincent Aranega and Stéphane Ducasse and Guillermo Polito and Pablo Tesone},
title = {A VM-Agnostic and Backwards Compatible Protected Modifier for Dynamically-Typed Languages},
journal = {},
volume = {},
number = {},
articleno = {2},
numpages = {36},
doi = {10.22152/programming-journal.org/2024/8/2},
year = {2024},
}
Publisher's Version