uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Clarke, Dave
Publications (10 of 30) Show all publications
Patrignani, M., Ahmed, A. & Clarke, D. (2019). Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. ACM Computing Surveys, 51(6), Article ID 125.
Open this publication in new window or tab >>Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
2019 (English)In: ACM Computing Surveys, ISSN 0360-0300, E-ISSN 1557-7341, Vol. 51, no 6, article id 125Article in journal (Refereed) Published
Abstract [en]

Secure compilation is a discipline aimed at developing compilers that preserve the security properties of the source programs they take as input in the target programs they produce as output. This discipline is broad in scope. targeting languages with a variety of features (including objects, higher-order functions, dynamic memory allocation, call/cc, concurrency) and employing a range of different techniques to ensure that source-level security is preserved at the target level. This article provides a survey of the existing literature on formal approaches to secure compilation with a focus on those that prove fully abstract compilation, which has been the criterion adopted by much of the literature thus far. This article then describes the formal techniques employed to prove secure compilation in existing work, introducing relevant terminology, and discussing the merits and limitations of each work. Finally, this article discusses open challenges and possible directions for future work in secure compilation.

Keywords
Secure compilation, fully abstract compilation, type preserving compilation, contextual equivalence, program equivalence
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-379940 (URN)10.1145/3280984 (DOI)000460376100016 ()
Funder
EU, European Research Council, 715753
Available from: 2019-03-26 Created: 2019-03-26 Last updated: 2019-03-26Bibliographically approved
Castegren, E., Clarke, D., Fernandez-Reyes, K., Wrigstad, T. & Yang, A. M. (2018). Attached and Detached Closures in Actors. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control: . Paper presented at AGERE'18 (8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control), Boston, MA, USA, November 05, 2018 (pp. 54-61). ACM Digital Library
Open this publication in new window or tab >>Attached and Detached Closures in Actors
Show others...
2018 (English)In: Proceedings of the 8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control, ACM Digital Library, 2018, p. 54-61Conference paper, Published paper (Refereed)
Abstract [en]

Expressive actor models combine aspects of functional programming into the pure actor model enriched with futures. Such functional features include first-class closures which can be passed between actors and chained on futures. Combined with mutable objects, this opens the door to race conditions. In some situations, closures may not be evaluated by the actor that created them yet may access fields or objects owned by that actor. In other situations, closures may be safely fired off to run as a separate task.

This paper discusses the problem of who can safely evaluate a closure to avoid race conditions, and presents the current solution to the problem adopted by the Encore language. The solution integrates with Encore's capability type system, which influences whether a closure is attached and must be evaluated by the creating actor, or whether it can be detached and evaluated independently of its creator.

Encore's current solution to this problem is not final or optimal. We conclude by discussing a number of open problems related to dealing with closures in the actor model.

Place, publisher, year, edition, pages
ACM Digital Library, 2018
Keywords
closures, parallel programming, concurrent programming, type systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-367318 (URN)10.1145/3281366.3281371 (DOI)000458146800006 ()978-1-4503-6066-1 (ISBN)
Conference
AGERE'18 (8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control), Boston, MA, USA, November 05, 2018
Funder
Swedish Research Council, 2012-4967Swedish Research Council, 2014-05545
Available from: 2018-11-29 Created: 2018-11-29 Last updated: 2019-02-28Bibliographically approved
Fernandez-Reyes, K., Clarke, D., Castegren, E. & Vo, H.-P. (2018). Forward to a Promising Future. In: Conference proceedings COORDINATION 2018: . Paper presented at COORDINATION - 20th International Conference on Coordination Models and Languages, Madrid, June 18-21, 2018..
Open this publication in new window or tab >>Forward to a Promising Future
2018 (English)In: Conference proceedings COORDINATION 2018, 2018Conference paper, Published paper (Refereed)
Abstract [en]

In many actor-based programming models, asynchronous method calls communicate their results using futures, where the fulfilment occurs under-the-hood. Promises play a similar role to futures, except that they must be explicitly created and explicitly fulfilled; this makes promises more flexible than futures, though promises lack fulfilment guarantees: they can be fulfilled once, multiple times or not at all. Unfortunately, futures are too rigid to exploit many available concurrent and parallel patterns. For instance, many computations block on a future to get its result only to return that result immediately (to fulfil their own future). To make futures more flexible, we explore a construct, forward, that delegates the responsibility for fulfilling the current implicit future to another computation. Forward reduces synchronisation and gives futures promise-like capabilities. This paper presents a formalisation of the forward construct, defined in a high-level source language, and a compilation strategy from the high-level language to a low-level, promised-based target language. The translation is shown to preserve semantics. Based on this foundation, we describe the implementation of forward in the parallel, actor-based language Encore, which compiles to C.

Keywords
parallel, concurrency, futures, actors, tasks
National Category
Computer Systems
Identifiers
urn:nbn:se:uu:diva-351352 (URN)
Conference
COORDINATION - 20th International Conference on Coordination Models and Languages, Madrid, June 18-21, 2018.
Available from: 2018-05-23 Created: 2018-05-23 Last updated: 2018-05-24Bibliographically approved
Fernandez-Reyes, K., Clarke, D. & Hornbach, J. (2018). The impact of opt-in gamification on students' grades in a software design course. In: Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings: . Paper presented at EduSymp MODELS ’18 Companion, October 14–19, 2018, Copenhagen, Denmark. New York, NY, USA: ACM Publications
Open this publication in new window or tab >>The impact of opt-in gamification on students' grades in a software design course
2018 (English)In: Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, New York, NY, USA: ACM Publications, 2018, p. -97Conference paper, Published paper (Refereed)
Abstract [en]

An achievement-driven methodology strives to give students more control of their learning with enough flexibility to engage them in deeper learning.

We observed in the course Advanced Software Design, which uses the achievement-driven methodology, that students fail to get high grades, which may hamper deeper learning. To motivate students to pursue and get higher grades we added gamification elements to the course.

To measure the success of our gamification implementation, students filled out a questionaire rating the enjoyment and motivation produced by the game. We built a statistical regression model where enjoyment and motivation explain 55% of the variation in grades. However, only the relationship between motivation and grade is significant, which implies that notivation drives the overall effect of the model. The results suggest that the more the students were motivated by the game, the higher their grades on the course (and vice versa). This implies that if gamification indeed motivates students, then it makes them go beyond what is expected.

Place, publisher, year, edition, pages
New York, NY, USA: ACM Publications, 2018
Keywords
software engineering, uml
National Category
Computer Systems
Research subject
Computer Science with specialization in Computer Science Education Research
Identifiers
urn:nbn:se:uu:diva-363142 (URN)10.1145/3270112.3270118 (DOI)978-1-4503-5965-8 (ISBN)
Conference
EduSymp MODELS ’18 Companion, October 14–19, 2018, Copenhagen, Denmark
Available from: 2018-10-14 Created: 2018-10-14 Last updated: 2018-10-15Bibliographically approved
Fernandez-Reyes, K. & Clarke, D. (2017). Affine killing: Semantics for stopping the ParT. In: Proc. 2nd International Workshop on Type-Driven Development: . Paper presented at TyDe 2017, September 3, Oxford, UK. New York: ACM Press
Open this publication in new window or tab >>Affine killing: Semantics for stopping the ParT
2017 (English)In: Proc. 2nd International Workshop on Type-Driven Development, New York: ACM Press, 2017Conference paper, Oral presentation with published abstract (Refereed)
Abstract [en]

Speculative, parallel abstractions allow that, once a result is computed, the remaining (unnecessary) speculative computations can be safely stopped. However, it is difficult to know when it is safe to stop an ongoing computation. This paper presents a refinement of the parallel speculative ParT abstraction with an affine type system that allows in-place updates, and killing speculative computations using thread-local reasoning. There is ongoing work to prove the soundness of the calculus and implement it in the Encore language.

Place, publisher, year, edition, pages
New York: ACM Press, 2017
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-326193 (URN)
Conference
TyDe 2017, September 3, Oxford, UK
Available from: 2017-07-04 Created: 2017-07-04 Last updated: 2018-01-13Bibliographically approved
Proenca, J. & Clarke, D. (2017). Typed connector families and their semantics. Science of Computer Programming, 146, 28-49
Open this publication in new window or tab >>Typed connector families and their semantics
2017 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 146, p. 28-49Article in journal (Refereed) Published
Abstract [en]

Typed models of connector/component composition specify interfaces describing ports of components and connectors. Typing ensures that these ports are plugged together appropriately, so that data can flow out of each output port and into an input port. These interfaces typically consider the direction of data flow and the type of values flowing. Components, connectors, and systems are often parameterised in such a way that the parameters affect the interfaces. Typing such connector families is challenging. This paper takes a first step towards addressing this problem by presenting a calculus of connector families with integer and boolean parameters. The calculus is based on monoidal categories, with a dependent type system that describes the parameterised interfaces of these connectors. We use families of Reo connectors as running examples, and show how this calculus can be applied to Petri Nets and to BIP systems. The paper focuses on the structure of connectors-well-connectedness-and less on their behaviour, making it easily applicable to a wide range of coordination and component-based models. A type-checking algorithm based on constraints is used to analyse connector families, supported by a proof of-concept implementation.

Keywords
Calculus of connectors, Variability in connectors, Composition of families, Type system, Tile Model
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-361062 (URN)10.1016/j.scico.2017.03.002 (DOI)000407402500003 ()
Available from: 2018-09-21 Created: 2018-09-21 Last updated: 2018-09-21Bibliographically approved
Broch Johnsen, E., Owe, O., Clarke, D. & Bjørk, J. (2016). A formal model of service-oriented dynamic object groups. Science of Computer Programming, 115–116, 3-22
Open this publication in new window or tab >>A formal model of service-oriented dynamic object groups
2016 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, p. 3-22Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-274432 (URN)10.1016/j.scico.2014.11.014 (DOI)000367122200002 ()
Funder
EU, FP7, Seventh Framework Programme, FP7-610582EU, FP7, Seventh Framework Programme, FP7-612985
Available from: 2014-12-04 Created: 2016-01-21 Last updated: 2018-01-10Bibliographically approved
Jongmans, S.-S. T. Q., Clarke, D. & Proença, J. (2016). A procedure for splitting data-aware processes and its application to coordination. Science of Computer Programming, 115–116, 47-78
Open this publication in new window or tab >>A procedure for splitting data-aware processes and its application to coordination
2016 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, p. 47-78Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-309773 (URN)10.1016/j.scico.2014.02.017 (DOI)
Available from: 2014-02-28 Created: 2016-12-07 Last updated: 2018-01-13Bibliographically approved
Muschevici, R., Proença, J. & Clarke, D. (2016). Feature Nets: Behavioural modelling of software product lines. Software and Systems Modeling, 15(4), 1181-1206
Open this publication in new window or tab >>Feature Nets: Behavioural modelling of software product lines
2016 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 15, no 4, p. 1181-1206Article in journal (Refereed) Published
Abstract [en]

Software product lines (SPLs) are diverse systems that are developed using a dual engineering process: (a) family engineering defines the commonality and variability among all members of the SPL, and (b) application engineering derives specific products based on the common foundation combined with a variable selection of features. The number of derivable products in an SPL can thus be exponential in the number of features. This inherent complexity poses two main challenges when it comes to modelling: firstly, the formalism used for modelling SPLs needs to be modular and scalable. Secondly, it should ensure that all products behave correctly by providing the ability to analyse and verify complex models efficiently. In this paper, we propose to integrate an established modelling formalism (Petri nets) with the domain of software product line engineering. To this end, we extend Petri nets to Feature Nets. While Petri nets provide a framework for formally modelling and verifying single software systems, Feature Nets offer the same sort of benefits for software product lines. We show how SPLs can be modelled in an incremental, modular fashion using Feature Nets, provide a Feature Nets variant that supports modelling dynamic SPLs, and propose an analysis method for SPL modelled as Feature Nets. By facilitating the construction of a single model that includes the various behaviours exhibited by the products in an SPL, we make a significant step towards efficient and practical quality assurance methods for software product lines.

Keywords
Behavioural modelling; Software product lines; Petri nets; Variability
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-268742 (URN)10.1007/s10270-015-0475-z (DOI)000384535800013 ()
Projects
UPMARC
Available from: 2015-06-17 Created: 2015-12-09 Last updated: 2018-01-10Bibliographically approved
Larmuseau, A., Patrignani, M. & Clarke, D. (2016). Implementing a secure abstract machine. In: Proc. 31st ACM Symposium on Applied Computing: . Paper presented at SAC 2016, April 4–8, Pisa, Italy (pp. 2041-2048). New York: ACM Press
Open this publication in new window or tab >>Implementing a secure abstract machine
2016 (English)In: Proc. 31st ACM Symposium on Applied Computing, New York: ACM Press, 2016, p. 2041-2048Conference paper, Published paper (Refereed)
Abstract [en]

Abstract machines are both theoretical models used to study language properties and practical models of language implementations. As with all language implementations, abstract machines are subject to security violations by the context in which they reside. This paper presents the implementation of an abstract machine for ML that preserves the abstractions of ML, in possibly malicious, low-level contexts. To guarantee this security result, we make use of a low-level memory isolation mechanism and derive the formalisation of the machine through a methodology, whose every step is accompanied by formal properties that ensure that the step has been carried out properly. We provide an implementation of the abstract machine and analyse its performance.

Place, publisher, year, edition, pages
New York: ACM Press, 2016
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-283165 (URN)10.1145/2851613.2851796 (DOI)978-1-4503-3739-7 (ISBN)
Conference
SAC 2016, April 4–8, Pisa, Italy
Projects
ProFuN
Available from: 2016-04-11 Created: 2016-04-11 Last updated: 2018-01-10
Organisations

Search in DiVA

Show all publications