58 research outputs found
Static safety guarantees for concurrent programming languages
No full text64 σ.Ο πολυνηματικός προγραμματισμός είναι ένα ευρέως χρησιμοποιούμενο πρότυπο προγραμματισμού για την αξιοποίηση του ταυτοχρονισμού σε πολυπύρηνα συστήματα. Μια εγγενής παρενέργεια αυτού του προτύπου είναι η μη ντετερμινιστική εκτέλεση των νημάτων. Σε αυτή την διατριβή δείχνουμε ότι είναι δυνατό να αυξηθεί η αξιοπιστία των ταυτόχρονων προγραμμάτων, με την εξάλειψη των παραβιάσεων πρόσβασης μνήμης, συνθηκών ανταγωνισμού και αδιεξόδων από πολυνηματικά προγράμματα. Συγκεκριμένα, παρουσιάζουμε την θεωρία και υλοποίηση συστημάτων τύπων (type systems) και στατικών αναλύσεων (static analyses) που παρέχουν κάποιες εγγυήσεις αξιοπιστίας σχετικά με την πολυνηματική εκτέλεση προγραμμάτων. Επίσης παρουσιάζουμε εκτεταμένες μετρήσεις για την απόδοση των αναλύσεών μας.Multi-threaded programming is widely used for enabling concurrency in multi-core architectures. An inherent side-effect of multi-threaded programming is the non-deterministic execution of threads. In this thesis we show that the reliability of concurrent programs can be increased by eliminating memory errors, data races and deadlocks from multi-threaded programs. Importantly, we present the theory and implementation of type system and static analyses that guarantee reliable execution of multi-threaded programs as well as some very promising benchmarks.Πρόδρομος Ε. Γερακιό
Α 12th-century \u27Platonic\u27 Dialogue: Theodoros Prodromos\u27 Xenedemos or Voices
No full textTheodoros Prodromos was a prominent intellectual of twelfth-century Byzantium. Among his substantial literary output a charming little dialogue bearing the title Xenedemos is to be found. The text tells us the story of the encounter between Xenedemos, a promising young student of philosophy, and Theokles, the leading philosopher of his time. Ιn the course of the discussion Theokles \u27deconstructs\u27 the definitions of the five logical categories offered in Porphyrios\u27 Introduction (Isagoge) and thereby seems to demolish its validity as a textbook for logic. Xenedemos is reasonably reduced to a state of intellectual perplexity (aporia) but is assured by his interlocutor that this is only due to his inexperience in dialectics and that he will eventually succeed in commanding the highest notions of philosophy.Α number of evidence proves that Prodromos consciously had his own piece moulded out of the Platonic matrix. Formal features, narrative techniques, structural correspondences and \u27 stage-directions\u27 indicate that the Byzantine piece employs as subtexts dialogues such as the Phaedo, the Parmenides and the Theaetetus. Significantly, Prodromos avoids any slavish imitation of his model but chooses to refashion the tradition of dialogue-writing established by Plato in terms of twelfth-century literary parlour. This choice is in itself interesting and telling of the expectations of Prodromos\u27 intended audience, especially if the Xenedemos was indeed meant as a eulogy in the memory of the author\u27s beloved teacher and a well-known Platonist, namely Michael Italikos.Theodoros Prodromos was a prominent intellectual of twelfth-century Byzantium. Among his substantial literary output a charming little dialogue bearing the title Xenedemos is to be found. The text tells us the story of the encounter between Xenedemos, a promising young student of philosophy, and Theokles, the leading philosopher of his time. Ιn the course of the discussion Theokles \u27deconstructs\u27 the definitions of the five logical categories offered in Porphyrios\u27 Introduction (Isagoge) and thereby seems to demolish its validity as a textbook for logic. Xenedemos is reasonably reduced to a state of intellectual perplexity (aporia) but is assured by his interlocutor that this is only due to his inexperience in dialectics and that he will eventually succeed in commanding the highest notions of philosophy.Α number of evidence proves that Prodromos consciously had his own piece moulded out of the Platonic matrix. Formal features, narrative techniques, structural correspondences and \u27 stage-directions\u27 indicate that the Byzantine piece employs as subtexts dialogues such as the Phaedo, the Parmenides and the Theaetetus. Significantly, Prodromos avoids any slavish imitation of his model but chooses to refashion the tradition of dialogue-writing established by Plato in terms of twelfth-century literary parlour. This choice is in itself interesting and telling of the expectations of Prodromos\u27 intended audience, especially if the Xenedemos was indeed meant as a eulogy in the memory of the author\u27s beloved teacher and a well-known Platonist, namely Michael Italikos
Eustathios at Prodromos Petra? Some Remarks on the Manuscript Tradition of the Exegesis in Canonem Iambicum Pentecostalem
No full textIn investigating the manuscript tradition of the Exegesis in canonem iambicum pentecostalem, two features emerge with a high degree of likelihood: (a) the relationship of the work with the monastery of Prodromos Petra at Constantinople; (b) the relationship of Eustathios himself with that same monastery during his tenure as professor in the Polis.
The article shows the manuscript tradition of Eustathius’ Exegesis: 5 manuscripts are described in detail, including their provenance along with their possessors: Vaticanus graecus 1409, Alexandrinus Patriarchalis 62 (107), Basileensis A.VII.1 (gr. 34), Vallicellianus F 44 (gr. 94), Vindobonensis Theol. Graec. 208 Nessel (298 Lambecius). Along with a thorough autoptical study, the reader finds here some improvements in Byzantine palaeography and philology. Then the author sheds light on the deperditus ms. Scorialensis Λ.II.11, once owned by Diego Hurtado de Mendoza and disappeared after the fire of Escorial in 1671. The codex is likely to have come from the Constantinopolitan monastery of Prodromos Petra, as well as the Vaticanus and the Alexandrinus. Positive clues of a provenance from Prodromos Petra are detected in the fragmentary tradition of the text and in further evidence: textual criticism has definitely revealed a sub-archetype Beta (β), most likely written before the Latin occupation of Constantinople in 1204. The dating and content of Beta seem to coincide with those of the deperditus ms. Scorialensis mentioned above, where codicological and philological data attest to a highest quality of the text, including its title.
Thus the second section of the article deals with the so-called didaskaleion of Prodromos Petra, its cultivated readers, mouseion and scriptorium, up to Georgius Baiophorus and his interventions in the ms of Basilea in 15th century. The first known official mention of the katholikon mouseion of Prodromos Petra is that of Francesco Filelfo; on his part, Eustathios writes he was asked to compose the Exegesis by an anonymous colleague, and that it was intended for advanced rhetorical and ecclesiastical instruction. Moreover, Eustathios’ reference to the name of Moses as related to the word “mouseion” provides us with a demonstration about lessons in 12th-century Constantinople, along with ironically equating himself with God teaching Moses on the mount Sinai. The very same identification is made by Michael Choniates about Eustathios in the funeral monody dedicated to him: hardly a coincidence.
Eustathios’ presence at the monastery is not documented at Prodromos Petra in the course of the 12th century. However, his acquaintance with that monastic milieu is apparent in a famous passage of the De emendanda vita monachica, where he lampoons the abundance of caviar for the emperor. Hardly a coincidence, again, that this is the absolutely first mention of Prodromos Petra found in literary sources
Il μουσεῖον di Prodromos Petra e una famiglia mononucleare di codici di Eustazio
No full textThis contribution attempts to investigate a family of five manuscripts, which, partially or entirely, transmits what is likely to be the last work of Eustathios of Thessaloniki: the Exegesis in canonem iambicum pentecostalem, i.e. a thorough commentary on one of the canons of Cosma’s and John’s corpus, in keep with the high standard of Eustathian previous teaching style. The author bases her argument onto two levels. Firstly, on philological, codicological and paleographical grounds, the author argues that the entirety of the manuscript tradition depends on a single subarchetype β, which she proposes to identify with the deperditus Scorialensis L.II.11. Secondly, by reconstructing the historia codicum of the surviving members of the family, she demonstrates that most of the exemplars can be traced back to the library, the scriptorium and probably also to that centre of teaching and cultural transmission that was the μουσεῖον of the Constantinopolitan monastery of Prodromos Petra. More specifically, the author hypothesizes that (a) β might be the last tome of an authorisierte Eustathiosedition, the existence of which was conjectured by Peter Wirth; (b) that it was to be found in Prodromos Petra as early as the second half of the 1190s, as already put forward suo Marte by Ernst Gamillscheg; (c) and that, preserved there during the Latin occupation of the Fourth Crusade, such exemplar generated the manuscript tradition of the Exegesis shortly after the Byzantine reconquest of the Polis. Combined with the appraisal of the aliae manus and their glosses, which over the centuries were added to the main text, this analysis suggests that in the same monastery survived, at an extracurricular level, that high profile rhetorical-ecclesiastical teaching based on the exegesis of the hymnographic corpus of Cosmas and John, which the Eustathian work testifies to, and which deteriorated after the transfer of the Patriarchal institutions to Nicaea, but could have been even previously set in the μουσεῖον of Prodromos Petra, whose familiarity to Eustathius himself has been shown by the author in an earlier contribution. It can be inferred that the floruit of the μονή τοῦ Προδρόμου not only as a monastic institution, a library and a scriptorium, but also as a leading university centre, in which the best scholars of Constantinople taught, could be placed before the Paleologan re-establishment, and perhaps as early as the XII century
A Concurrent Language with a Uniform Treatment of Regions and Locks
No full textA challenge for programming language research is to design and implement multi-threaded low-level languages providing static guarantees for memory safety and freedom from data races. Towards this goal, we present a concurrent language employing safe region-based memory management and hierarchical locking of regions. Both regions and locks are treated uniformly, and the language supports ownership transfer, early deallocation of regions and early release of locks in a safe manner
Race-free and memory-safe multithreading: Design and implementation in cyclone
No full textWe present the design of a formal low-level multi-threaded lan-guage with advanced region-based memory management and syn-chronization primitives, where well-typed programs are memory safe and race free. In our language, regions and locks are combined in a single hierarchy and are subject to uniform ownership con-straints imposed by a hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is protected, then its sub-regions are also protected. We discuss as-pects of the integration and implementation of the formal language within Cyclone and evaluate the performance of code produced by the modified Cyclone compiler against highly optimized C pro-grams using atomic operations, pthreads, and OpenMP. Although our implementation is still in a preliminary stage, our results show that the performance overhead for guaranteed race freedom and memory safety is acceptable
Forsaking Inheritance: Supercharged Delegation in DelphJ
No full textWe propose DelphJ: a Java-based OO language that eschews inheritance completely, in favor of a combination of class morphing and (deep) delegation. Compared to past delegation approaches, the novel aspect of our design is the ability to emulate the best aspects of inheritance while retaining maximum flexibility: using morphing, a class can select any of the methods of its delegatee and export them (if desired) or transform them (e.g., to add extra arguments or modify type signatures), yet without needing to name these methods explicitly and handle them one-by-one. Compared to past work on morphing, our approach adopts and adapts advanced delegation mechanisms, in order to add late binding capabilities and, thus, provide a full substitute of inheritance. Additionally, we explore complex semantic issues in the interaction of delegation with late binding. We present our language design both informally, with numerous examples, and formally in a core calculus
Foo: A Minimal Modern OO Calculus
No full textWe present the Flyweight Object-Oriented (Foo) calculus for the modeling of object-oriented languages. Foo is a simple, minimal class-based calculus, modeling only essential computational aspects and emphasizing larger-scale features (e.g., inheritance and generics). Foo is motivated by the observation that recent language design work focuses on elements not well-captured either by traditional object calculi or by language-specific modeling efforts, such as Featherweight Java. Foo integrates seamlessly both nominal and structural subtyping ideas, leveraging the latter to eliminate the need for modeling object fields and constructors. Comparing to recent formalization efforts in the literature, Foo is more compact, yet versatile enough to be usable in multiple settings modeling Java, C#, or Scala extensions
Forsaking Inheritance: Supercharged Delegation in DelphJ
No full textWe propose DelphJ: a Java-based OO language that eschews
inheritance completely, in favor of a combination of class
morphing and (deep) delegation. Compared to past delegation approaches, the novel aspect of our design is the ability to emulate the best aspects of inheritance while retaining
maximum flexibility: using morphing, a class can select any
of the methods of its delegatee and export them (if desired)
or transform them (e.g., to add extra arguments or modify
type signatures), yet without needing to name these meth-
ods explicitly and handle them one-by-one. Compared to
past work on morphing, our approach adopts and adapts advanced delegation mechanisms, in order to add late binding
capabilities and, thus, provide a full substitute of inheritance.
Additionally, we explore complex semantic issues in the interaction of delegation with late binding. We present our language design both informally, with numerous examples, and
formally in a core calculus
- …
