uu.seUppsala universitets publikasjoner
Endre søk
Begrens søket
12 1 - 50 of 89
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Comparing source sets and persistent sets for partial order reduction2017Inngår i: Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Springer, 2017, s. 516-536Kapittel i bok, del av antologi (Annet vitenskapelig)
    Abstract [en]

    Partial order reduction has traditionally been based on persistent sets, ample sets, stubborn sets, or variants thereof. Recently, we have presented a strengthening of this foundation, using source sets instead of persistent/ample/stubborn sets. Source sets subsume persistent sets and are often smaller than persistent sets. We introduced source sets as a basis for Dynamic Partial Order Reduction (DPOR), in a framework which assumes that processes are deterministic and that all program executions are finite. In this paper, show how to use source sets for partial order reduction in a framework which does not impose these restrictions. We also compare source sets with persistent sets, providing some insights into conditions under which source sets and persistent sets do or do not differ.

  • 2.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Optimal dynamic partial order reduction2014Inngår i: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York: ACM Press, 2014, s. 373-384Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.

  • 3.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction2017Inngår i: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, nr 4, artikkel-id 25Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source-and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.

  • 4.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Lång, Magnus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ngo, Tuan-Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Optimal stateless model checking for reads-from equivalence under sequential consistency2019Inngår i: Proceedings of the ACM on programming languages, ISSN 2475-1421Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a new approach for stateless model checking (SMC) of multithreaded programs under Sequential Consistency (SC) semantics.  To combat state-space explosion, SMC is often equipped with a partial-order reduction technique, which defines an equivalence on executions, and only needs to explore one execution in each equivalence class.  Recently, it has been observed that the commonly used equivalence of Mazurkiewicz traces can be coarsened but still cover all program crashes and assertion violations.  However, for this coarser equivalence, which preserves only the reads-from relation from writes to reads, there is no SMC algorithm which is (i) optimal in the sense that it explores precisely one execution in each reads-from equivalence class, and (ii) efficient in the sense that it spends polynomial effort per class.  \end{inparaenum} We present the first SMC algorithm for SC that is both optimal and efficient in practice, meaning that it spends polynomial time per equivalence class on all programs that we have tried.  This is achieved by a novel test that checks whether a given reads-from relation can arise in some execution.  Our experimental results show that Nidhugg/rfsc, although slower than the fastest SMC tools in programs where tools happen to examine the same number of executions, always scales similarly or better than them, and outperforms them by an exponential factor in programs where the reads-from equivalence is coarser than the standard one. We also present two non-trivial use cases where the new equivalence is particularly effective, as well as the significant performance advantage that Nidhugg/rfsc offers compared to state-of-the-art SMC and systematic concurrency testing tools.

  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Leonardsson, Carl
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Stateless model checking for TSO and PSO2015Inngår i: Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, Springer Berlin/Heidelberg, 2015, s. 353-367Konferansepaper (Fagfellevurdert)
  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Leonardsson, Carl
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Stateless model checking for TSO and PSO2017Inngår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 54, nr 8, s. 789-818Artikkel i tidsskrift (Fagfellevurdert)
  • 7.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Lång, Magnus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Optimal dynamic partial order reduction with observers2018Inngår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, s. 229-248Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks.

  • 8.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Papaspyrou, Nikolaos
    Roukounaki, Katerina
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Tsiouris, Yiannis
    Venetis, Ioannis E.
    A scalability benchmark suite for Erlang/OTP2012Inngår i: Proc. 11th ACM SIGPLAN Workshop on Erlang, New York: ACM Press, 2012, s. 33-42Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Programming language implementers rely heavily on benchmarking for measuring and understanding performance of algorithms, architectural designs, and trade-offs between alternative implementations of compilers, runtime systems, and virtual machine components. Given this fact, it seems a bit ironic that it is often more difficult to come up with a good benchmark suite than a good implementation of a programming language.

    This paper presents the main aspects of the design and the current status of bencherl, a publicly available scalability benchmark suite for applications written in Erlang. In contrast to other benchmark suites, which are usually designed to report a particular performance point, our benchmark suite aims to assess scalability, i.e., help developers to study a set of performance points that show how an application's performance changes when additional resources (e.g., CPU cores, schedulers, etc.) are added. We describe the scalability dimensions that the suite aims to examine and present its infrastructure and current set of benchmarks. We also report some limited set of performance results in order to show the capabilities of our suite.

  • 9.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    On using Erlang for parallelization: Experience from parallelizing Dialyzer2013Inngår i: Trends in Functional Programming, Springer Berlin/Heidelberg, 2013, s. 295-310Konferansepaper (Fagfellevurdert)
  • 10.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The shared-memory interferences of Erlang/OTP built-ins2017Inngår i: Proceedings Of The 16Th Acm Sigplan International Workshop On Erlang (Erlang '17) / [ed] Chechina, N.; Fritchie, SL., New York: Association for Computing Machinery (ACM), 2017, s. 43-54Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Erlang is a concurrent functional language based on the actor modelof concurrency. In the purest form of this model, actors are realizedby processes that do not share memory and communicate witheach other exclusively via message passing. Erlang comes quiteclose to this model, as message passing is the primary form of interprocesscommunication and each process has its own memoryarea that is managed by the process itself. For this reason, Erlangis often referred to as implementing “shared nothing” concurrency.Although this is a convenient abstraction, in reality Erlang’s mainimplementation, the Erlang/OTP system, comes with a large numberof built-in operations that access memory which is shared byprocesses. In this paper, we categorize these built-ins, and characterizethe interferences between them that can result in observabledifferences of program behaviour when these built-ins are usedin a concurrent setting. The paper is complemented by a publiclyavailable suite of more than one hundred small Erlang programsthat demonstrate the racing behaviour of these built-ins.

  • 11.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lystig Fritchie, Scott
    VMware, Cambridge, MA, USA.
    Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking2017Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

  • 12.
    Asai, Kenichi
    et al.
    Ochanomizu Univ, Tokyo 112, Japan..
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. NTUA, Athens, Greece..
    Selected and extended papers from Partial Evaluation and Program Manipulation 2015 (PEPM ' 15)2017Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 137, s. 1-1Artikkel i tidsskrift (Annet vitenskapelig)
  • 13. Boudeville, Olivier
    et al.
    Cesarini, Francesco
    Chechina, Natalia
    Lundin, Kenneth
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Thompson, Simon
    Trinder, Phil
    Wiger, Ulf
    RELEASE: A high-level paradigm for reliable large-scale server software2013Inngår i: Trends in Functional Programming, Springer Berlin/Heidelberg, 2013, s. 263-278Konferansepaper (Fagfellevurdert)
  • 14.
    Carlsson, Richard
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Wilhelmsson, Jesper
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Message Analysis for Concurrent Languages2003Inngår i: In Proceedings of the Static Analysis Symposium, 2003, s. 73-90Konferansepaper (Fagfellevurdert)
  • 15.
    Carlsson, Richard
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Wilhelmsson, Jesper
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Message analysis for concurrent programs using message passing2006Inngår i: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 28, nr 4, s. 715-746Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We describe an analysis-driven storage allocation scheme for concurrent systems that use message passing with copying semantics. The basic principle is that in such a system, data which is not part of any message does not need to be allocated in a shared data area. This allows for the deallocation of thread-specific data without requiring global synchronization and often without even triggering garbage collection. On the other hand, data that is part of a message should preferably be allocated on a shared area since this allows for fast (O(1)) interprocess communication that does not require actual copying. In the context of a dynamically typed, higher-order concurrent functional language, we present a static message analysis which guides the allocation. As shown by our performance evaluation, conducted using a production-quality language implementation, the analysis is effective enough to discover most data which is to be used as a message, and to allow the allocation scheme to combine the best performance characteristics of both a process-centric and a communal memory architecture.

  • 16.
    Christakis, Maria
    et al.
    ETH Zurich.
    Gotovos, Alkis
    ETH Zurich.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Systematic testing for detecting concurrency errors in Erlang programs2013Inngår i: Proc. 6th International Conference on Software Testing, Verification and Validation, IEEE Computer Society, 2013, s. 154-163Konferansepaper (Fagfellevurdert)
  • 17. Christakis, Maria
    et al.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Detection of asynchronous message passing errors using static analysis2011Inngår i: Practical Aspects of Declarative Languages, Springer Berlin/Heidelberg, 2011, s. 5-18Konferansepaper (Fagfellevurdert)
  • 18. Christakis, Maria
    et al.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Static detection of race conditions in Erlang2010Inngår i: Practical Aspects of Declarative Languages: PADL 2010, Berlin: Springer-Verlag , 2010, s. 119-133Konferansepaper (Fagfellevurdert)
  • 19. Demoen, Bart
    et al.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    CAT: the Copying Approach to Tabling1999Inngår i: Journal of Functional and Logic Programming: Special Issue on Selected Best Papers from PLILP/ALP'98, Vol. 1999, nr 2, s. 1-38Artikkel i tidsskrift (Fagfellevurdert)
  • 20. Demoen, Bart
    et al.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Heap Memory Management in Prolog with Tabling: Practice and Experience2001Inngår i: Journal of Functional and Logic Programming: Special Issue on Selected Best Papers from PADL 2000, Vol. 9, s. 1-56Artikkel i tidsskrift (Fagfellevurdert)
  • 21.
    Elsts, Atis
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Hassani Bijarbooneh, Farshid
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jacobsson, Martin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Enabling design of performance-controlled sensor network applications through task allocation and reallocation2015Inngår i: Proc. 11th International Conference on Distributed Computing in Sensor Systems, IEEE Computer Society, 2015, s. 248-253Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Task Graph (ATaG) is a sensor network application development paradigm where the application is visually described by a graph where the nodes correspond to application-level tasks and edges correspond to dataflows. We extend ATaG with the option to add nonfunctional requirements: constraints on end-to-end delay and packet delivery rate. Setting up these constraints at the design phase naturally leads to enabling run-time assurance at the deployment phase, when the conditions of the constraints are used as network's performance goals. We provide both run-time middleware that checks the conditions of these constraints and a central management unit that dynamically adapts the system by doing task reallocation and putting task copies on redundant nodes. Through extensive simulations we show that the system is efficient enough to enable adaptations within tens of seconds even in large networks.

  • 22.
    Elsts, Atis
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Hassani Bijarbooneh, Farshid
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jacobsson, Martin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    ProFuN TG: A tool for programming and managing performance-aware sensor network applications2015Inngår i: IEEE 40th Local Computer Networks Conference Workshops (LCN Workshops), IEEE Computer Society, 2015, s. 751-759Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Sensor network macroprogramming methodologiessuch as the Abstract Task Graph hold the promise of enablinghigh-level sensor network application development. However,progress in this area is hampered by the scarcity of tools, andalso because of insufficient focus on developing tool support forprogramming applications aware of performance requirements.

    We present ProFuN TG (Task Graph), a tool for designing sen-sor network applications using task graphs. ProFuN TG providesautomated task mapping, sensor node firmware macrocompila-tion, application simulation, deployment, and runtime mainte-nance capabilities. It allows users to incorporate performancerequirements in the applications, expressed through constraintson task-to-task dataflows. The tool includes middleware that usesan efficient flooding-based protocol to set up tasks in the network,and also enables runtime assurance by keeping track of theconstraint conditions.

    We show that the adaptive task reallocation enabled by ourapproach can significantly increase application reliability whiledecreasing energy consumption: in a network with unreliablelinks, we achieve above 99.89 % task-to-task PDR while keepingthe maximal radio duty cycle around 2.0 %.

  • 23.
    Elsts, Atis
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Hassani Bijarbooneh, Farshid
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jacobsson, Martin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    ProFuN TG: A Tool Using Abstract Task Graphs to Facilitate the Development, Deployment and Maintenance of Wireless Sensor Network Applications2015Inngår i: Proc. Poster/Demo Session: 12th European Conference on Wireless Sensor Networks, 2015, s. 19-20Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In this demo abstract we present ProFuN TG (Task Graph), a tool for sensor network application development using the data-flow programming paradigm. The tool has support for the whole lifecycle of WSN application: from the initial design of its task graph, task placement on network nodes, execution in a simulated environment, deployment on real hardware, to its automated maintenance through task remapping. ProFuN TG allows to program applications that incorporate quality-of-service requirements, expressed through constraints on task-to-task data flows.

  • 24.
    Elsts, Atis
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Hassani Bijarbooneh, Farshid
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jacobsson, Martin
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    ProFuN TG: Programming Sensornets with Task Graphs for Increased Reliability and Energy-Efficiency2015Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Sensor network macroprogramming methodologies such as the Abstract Task Graph hold the promise of enabling high-level sensor network application development. However, progress in this area is hampered by the scarcity of tools, and also because of insufficient focus on developing tool support for programming applications aware of performance requirements.

    In this demo we present ProFuN TG (Task Graph), a tool for designing sensor network applications using task graphs. ProFuN TG provides automated task mapping, sensor nodefirmware macrocompilation, application simulation, deployment, and runtime maintenance capabilities. It allows users to incorporate performance requirements in the applications, expressed through constraints on task-to-task dataflows. The tool includes middleware that uses an efficient flooding-based protocol to set up tasks in the network, and also enables runtime assurance by keeping track of the constraint conditions.

    Through task allocation in a way that optimizes an objective function in a model of the network, and adaptive task reallocation in case of link, node, or sensor failures the tool helps to make sensornet applications both more energy-efficient and reliable.

  • 25. Gerakios, Prodromos
    et al.
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    A concurrent language with a uniform treatment of regions and locks2010Inngår i: Proc. 2nd Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software: PLACES 2009, 2010, s. 79-93Konferansepaper (Fagfellevurdert)
  • 26. Gerakios, Prodromos
    et al.
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    A type and effect system for deadlock avoidance in low-level languages2011Inngår i: Proc. 6th International Workshop on Types in Language Design and Implementation, New York: ACM Press , 2011, s. 15-28Konferansepaper (Fagfellevurdert)
  • 27. Gerakios, Prodromos
    et al.
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Race-free and memory-safe multithreading: Design and implementation in Cyclone2010Inngår i: Proc. 5th International Workshop on Types in Language Design and Implementation, New York: ACM Press , 2010, s. 15-26Konferansepaper (Fagfellevurdert)
  • 28. Gerakios, Prodromos
    et al.
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Static safety guarantees for a low-level multithreaded language with regions2014Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 80, nr Part B, s. 223-263Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present the design of a formal low-level multithreaded language with advanced region-based memory management and thread synchronization 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 constraints imposed by this hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is read/write-protected, then its sub-regions inherit the same access rights. We discuss aspects 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 programs using pthreads. Our results show that the performance overhead for guaranteed race freedom and memory safety is in most cases acceptable.

  • 29.
    Giantsios, Aggelos
    et al.
    Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Papaspyrou, Nikolaos
    Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Concolic testing for functional languages2017Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 147, s. 109-134Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Concolic testing is a software testing technique that simultaneously combines concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that explore other paths, which gives better path coverage than random test case generation). So far, concolic testing has been applied, mainly at the level of bytecode or assembly code, to programs written in imperative languages that manipulate primitive data types such as integers and arrays. In this article, we demonstrate its application to a functional programming language core, the functional subset of Core Erlang, that supports pattern matching, structured recursive data types such as lists, recursion and higher-order functions. We present CutEr, a tool implementing this testing technique, and describe its architecture, the challenges that it needs to address, its current limitations, and report some experiences from its use.

  • 30.
    Gustafsson, Per
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Adaptive Pattern Matching on Binary Data2004Inngår i: In Programming Languages and Systems. Proceedings of the 13th European Symposium On Programming: Volume 2986 in LNCS, 2004, s. 124-139Konferansepaper (Fagfellevurdert)
  • 31.
    Gustafsson, Per
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Applications, Implementation and Performance Evaluation of Bit Stream Programming in Erlang2007Inngår i: Practical Aspects of Declarative Languages: PADL 2007 / [ed] Hanus, M, 2007, s. 94-108Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Writing code that manipulates bit streams is a painful and error-prone programming task, often performed via bit twiddling techniques such as explicit bit shifts and bit masks in programmer-allocated buffers. Still, this kind of programming is necessary in many application areas ranging from decoding streaming media files to implementing network protocols. In this paper we employ high-level constructs from declarative programming, such as pattern matching at the bit level and bit stream comprehensions, and show how a variety of bit stream programming applications can be written in a succinct, less error-prone, and totally memory-safe manner. We also describe how these constructs can be implemented efficiently. The resulting performance is superior to that of other (purely) functional languages and competitive to that of low-level languages such as C.

  • 32.
    Gustafsson, Per
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Bit-level Binaries and Generalized Comprehensions in Erlang2005Inngår i: Proceedings of the Fourth ACM SIGPLAN Erlang Workshop, 2005, s. 1-8Konferansepaper (Fagfellevurdert)
  • 33.
    Gustafsson, Per
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Native Code Compilation of Erlang's Bit Syntax2002Inngår i: Proceedings of the ACM SIGPLAN Erlang Workshop, Pittsburgh, Pennsylvania, 2002, s. 6-15Konferansepaper (Fagfellevurdert)
  • 34. Jiménez, Miguel
    et al.
    Lindahl, Tobias
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    A language for specifying type contracts in Erlang and its interaction with success typings2007Inngår i: Proc. 6th ACM SIGPLAN Workshop on ERLANG, New York: ACM Press , 2007, s. 11-17Konferansepaper (Fagfellevurdert)
  • 35.
    Johansson, Erik
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pettersson, Mikael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lindgren, Thomas
    The development of the HiPE system: Design and experience report2003Inngår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1385-4879, E-ISSN 1571-8115, Vol. 4, nr 4, s. 421-436Artikkel i tidsskrift (Fagfellevurdert)
  • 36.
    Johansson, Erik
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Linear Scan Register Allocation in a High-Performance Erlang Compiler.2002Inngår i: # Practical Aspects of Declarative Languages: Proceedings of the PADL 2002 Symposium, Portland, Oregon., 2002, s. 299-317Konferansepaper (Fagfellevurdert)
  • 37.
    Johansson, Erik
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Wilhelmsson, Jesper
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Heap Architectures for Concurrent Languages using Message Passing2002Inngår i: Proceedings of ISMM'2002: ACM SIGPLAN International Symposium on Memory Management, 2002, s. 88-99Konferansepaper (Fagfellevurdert)
  • 38.
    Jonsson, Bengt
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    ASTEC: An Experience in the Establishment of Collaboration between Academia and Industry2003Inngår i: Springer International Journal on Software Tools for Technology Transfer, Vol. 4, nr 4, s. 401-404Artikkel i tidsskrift (Fagfellevurdert)
  • 39.
    Kallas, Konstantinos
    et al.
    Univ Penn, Philadelphia, PA 19104 USA.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    HiPErJiT: A Profile-Driven Just-in-Time Compiler for Erlang2018Inngår i: Proceedings of the 30th Symposium on Implementation and Application ff Functional Languages (IFL 2018) / [ed] Cimini, M, Association for Computing Machinery (ACM), 2018, s. 25-36Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We introduce HiPErJiT, a profile-driven Just-in-Time compiler for the BEAM ecosystem based on HiPE, the High Performance Erlang compiler. HiPErJiT uses runtime profiling to decide which modules to compile to native code and which of their functions to inline and type-specialize. HiPErJiT is integrated with the runtime system of Erlang/OTP and preserves aspects of Erlang's compilation which are crucial for its applications: most notably, tail-call optimization and hot code loading at the module level. We present HiPErJiT's architecture, describe the optimizations that it performs, and compare its performance with BEAM, HiPE, and Pyrlang. HiPErJiT offers performance which is about two times faster than BEAM and almost as fast as HiPE, despite the profiling and compilation overhead that it has to pay compared to an ahead-of-time native code compiler. But there also exist programs for which HiPErJiT's profile-driven optimizations allow it to surpass HiPE's performance.

  • 40.
    Klaftenegger, David
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Winblad, Kjell
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Brief announcement: queue delegation locking2014Inngår i: Proc. 26th ACM Symposium on Parallelism in Algorithms and Architectures, New York: ACM Press, 2014, s. 70-72Konferansepaper (Fagfellevurdert)
  • 41.
    Klaftenegger, David
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Winblad, Kjell
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Delegation locking libraries for improved performance of multithreaded programs2014Inngår i: Euro-Par 2014: Parallel Processing, Springer Berlin/Heidelberg, 2014, Vol. 8632, s. 572-583Konferansepaper (Fagfellevurdert)
  • 42.
    Klaftenegger, David
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Winblad, Kjell
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    On the scalability of the Erlang term storage2013Inngår i: Proc. 12th ACM SIGPLAN Workshop on Erlang, New York: ACM Press, 2013, s. 15-26Konferansepaper (Fagfellevurdert)
  • 43.
    Klaftenegger, David
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Winblad, Kjell
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Queue Delegation Locking2018Inngår i: IEEE Transactions on Parallel and Distributed Systems, ISSN 1045-9219, E-ISSN 1558-2183, Vol. 29, nr 3, s. 687-704Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The scalability of parallel programs is often bounded by the performance of synchronization mechanisms used to protect critical sections. The performance of these mechanisms is in turn determined by their sequential execution time, efficient use of hardware, and ability to avoid waiting. In this article, we describe queue delegation (QD) locking, a family of locks that both delegate critical sections and enable detaching execution. Threads delegate work to the thread currently holding the lock and are able to detach, i.e., immediately continue their execution until they need a result from a previously delegated critical section. We show how to use queue delegation to build synchronization algorithms with lower overhead and higher throughput than existing algorithms, even when critical sections need to communicate results back immediately. Experiments when using up to 64 threads to access a shared priority queue show that QD locking provides 10 times higher throughput than Pthreads mutex locks and outperforms leading delegation algorithms. Also, when mixing parallel reads with delegated write operations, QD locking outperforms competing algorithms with an advantage ranging from 9.5 up to 207 percent increased throughput. Last but not least, continuing execution instead of waiting for the execution of critical sections leads to increased parallelism and better scalability. As we will see, queue delegation locking uses simple building blocks whose overhead is low even in uncontended use. All these make the technique useful in a wide variety of applications.

  • 44.
    Kokologiannakis, Michalis
    et al.
    National Technical University of Athens, Greece.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU)2017Inngår i: Proc. 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, New York: ACM Press, 2017, s. 172-181Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Read-Copy-Update (RCU) is a synchronization mechanism used heavily in key components of the Linux kernel, such as the virtual filesystem (VFS), to achieve scalability by exploiting RCU's ability to allow concurrent reads and updates. RCU's design is non-trivial, requires significant effort to fully understand it, let alone become convinced that its implementation is faithful to its specification and provides its claimed properties. The fact that as time goes by Linux kernels are becoming increasingly more complex and are employed in machines with more and more cores and weak memory does not make the situation any easier.

    This paper presents an approach to systematically test the code of the main flavor of RCU used in the Linux kernel (Tree RCU) for concurrency errors, both under sequential consistency and weak memory. Our modeling allows Nidhugg, a stateless model checking tool, to reproduce, within seconds, safety and liveness bugs that have been reported for RCU. More importantly, we were able to verify the Grace-Period guarantee, the basic guarantee that RCU offers, on several Linux kernel versions (non-preemptible builds). Our approach is effective, both in dealing with the increased complexity of recent Linux kernels and in terms of time that the process requires. We have good reasons to believe that our effort constitutes a big step towards making tools such as Nidhugg part of the standard testing infrastructure of the Linux kernel.

  • 45.
    Kokologiannakis, Michalis
    et al.
    Max Planck Inst Software Syst MPI SWS, Kaiserslautern Saarbruke, Germany.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Stateless model checking of the Linux kernel's read-copy update (RCU)2019Inngår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 21, nr 3, s. 287-306Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Read-copy update (RCU) is a synchronization mechanism used heavily in key components of the Linux kernel, such as the virtual filesystem (VFS), to achieve scalability by exploiting RCU's ability to allow concurrent reads and updates. RCU's design is non-trivial, requires a significant effort to fully understand it, let alone become convinced that its implementation is faithful to its specification and provides its claimed properties. The fact that as time goes by Linux kernels are becoming increasingly more complex and are employed in machines with more and more cores and weak memory does not make the situation any easier. This article presents an approach to systematically test the code of the main implementation of RCU used in the Linux kernel (Tree RCU) for concurrency errors, both under sequentially consistent and weak memory. Our modeling allows Nidhugg, a stateless model checking tool, to reproduce, within seconds, safety and liveness bugs that have been reported for RCU. Additionally, we present the real cause behind some failures that have been observed in production systems in the past. More importantly, we were able to verify both the publish-subscribe and the grace-period guarantee, with the latter being the basic and most important guarantee that RCU offers, on several Linux kernel versions, for particular configurations. Our approach is effective, both in dealing with the increased complexity of recent Linux kernels and in terms of time that the process requires. We hold that our effort constitutes a good first step toward making tools such as Nidhugg part of the standard testing infrastructure of the Linux kernel.

  • 46.
    Lindahl, Tobias
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Detecting Software Defects in Telecom Applications Through Lightweight Static Analysis: A War Story2004Inngår i: In Programming Languages and Systems: Proceedings of the Second Asian Symposium: Volume 3302 in LNCS, 2004, s. 91-106Konferansepaper (Fagfellevurdert)
  • 47.
    Lindahl, Tobias
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Practical type inference based on success typings2006Inngår i: Proc. 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2006, s. 167-178Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In languages where the compiler performs no static type checks, many programs never go wrong, but the intended use of functions and component interfaces is often undocumented or appears only in the form of comments which cannot always be trusted. This often makes program maintenance problematic. We show that it is possible to reconstruct a significant portion of the type information which is implicit in a program, automatically annotate function interfaces, and detect definite type clashes without fundamental changes to the philosophy of the language or imposing a type system which unnecessarily rejects perfectly reasonable programs. To do so, we introduce the notion of success typings of functions. Unlike most static type systems, success typings incorporate subtyping and never disallow a use of a function that will not result in a type clash during runtime. Unlike most soft typing systems that have previously been proposed, success typings allow for compositional, bottom-up type inference which appears to scale well in practice. Moreover, by taking control-flow into account and exploiting properties of the language such as its module system, success typings can be refined and become accurate and precise We demonstrate the power and practicality of the approach by applying it to Erlang. We report on our experiences from employing the type inference algorithm, without any guidance, on programs of significant size.

  • 48.
    Lindahl, Tobias
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. CSD.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Unboxed Compilation of Floating Point Arithmetic in a Dynamically Typed Language Environment.2002Inngår i: Proceedings of the 14th International Workshop on the Implementation of Functional Languages (IFL 2002). Madrid, Spain, September 2002. LNCS., 2002Konferansepaper (Fagfellevurdert)
  • 49.
    Luna, Daniel
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Pettersson, Mikael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi. Datalogi.
    Efficiently Compiling a Functional Language on AMD64: The HiPE Experience2005Inngår i: Proceedings of the Seventh ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, 2005, s. 176-186Konferansepaper (Fagfellevurdert)
  • 50.
    Luna, Daniel
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Pettersson, Mikael
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Teknisk-naturvetenskapliga fakulteten, Biologiska sektionen, Institutionen för ekologi och evolution, Datalogi.
    HiPE on AMD642004Inngår i: In Proceedings of the Third ACM SIGPLAN Erlang Workshop, 2004, s. 38-47Konferansepaper (Fagfellevurdert)
12 1 - 50 of 89
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf