uu.seUppsala University Publications
Change search
Refine search result
1234 1 - 50 of 176
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Oldest first
  • Newest first
Select
The maximal number of hits you can export is 250. When you want to export more records please use the 'Create feeds' function.
  • 1. Aarts, Fides
    et al.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Uijen, Johan
    Vaandrager, Frits
    Generating models of infinite-state communication protocols using regular inference with abstraction2015In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 46, no 1, 1-41 p.Article in journal (Refereed)
    Abstract [en]

    In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.

  • 2.
    Abdulla, Parosh
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Aronis, Stavros
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Sagonas, Konstantinos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Optimal dynamic partial order reduction2014In: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York: ACM Press, 2014, 373-384 p.Conference paper (Refereed)
    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 Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bouajjani, Ahmed
    Ngo, Tuan Phong
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Context-bounded analysis for POWER2017In: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2017, 56-74 p.Conference paper (Refereed)
  • 4.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bui, Phi Diep
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Counter-Example Guided Program Verification2016In: FM 2016: Formal Methods, Springer, 2016, 25-42 p.Conference paper (Refereed)
  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Chen, Yu-Fang
    Institute of Information Science, Academia Sinica .
    Holik, Lukas
    Brno University.
    Rezine, Ahmed
    Linköping University.
    Rümmer, Philipp
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    String Constraints for Verification2014In: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Springer, 2014, 150-166 p.Conference paper (Refereed)
    Abstract [en]

    We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.

  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Hofman, Piotr
    Mayr, Richard
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Totzke, Patrick
    Infinite-state energy games2014In: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, New York: ACM Press, 2014Conference paper (Refereed)
    Abstract [en]

    Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this.

    We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata.

    Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

  • 7.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Rezine, Othmane
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Verification of Directed Acyclic Ad Hoc Networks2013In: Formal Techniques for Distributed Systems: FORTE 2013, Springer Berlin/Heidelberg, 2013, 193-208 p.Conference paper (Refereed)
  • 8.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Stenman, Jari
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Zenoness for Timed Pushdown Automata2014In: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014, -47 p.Conference paper (Refereed)
    Abstract [en]

    Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.

  • 9.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Atig, Mohamed Faouzi
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Stenman, Jari
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Computing optimal reachability costs in priced dense-timed pushdown automata2014In: Language and Automata Theory and Applications: LATA 2014, Springer Berlin/Heidelberg, 2014, 62-75 p.Conference paper (Refereed)
  • 10.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Clemente, Lorenzo
    Mayr, Richard
    Sandberg, Sven
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Stochastic Parity Games on Lossy Channel Systems2014In: Logical Methods in Computer Science, ISSN 1860-5974, Vol. 10, no 4, 21Article in journal (Refereed)
    Abstract [en]

    We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, under the constraint that both players are restricted to finitememory strategies. First, we describe a general framework, where we consider the class of 21/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.

  • 11.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Dwarkadas, Sandhya
    University of Rochester, U.S.A..
    Rezine, Ahmed
    Linköping University.
    Shriraman, Arrvindh
    Simon Fraser University, Canada .
    Yunyun, Zhu
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Verifying safety and liveness for the FlexTM hybrid transactional memory2013Conference paper (Refereed)
    Abstract [en]

    We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations of transactional memories based on an adaptation of the MESI coherence protocol. FlexTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use of the latest antichain based techniques to handle systems with tens of thousands of states.

  • 12.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Haziza, Frédéric
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Holík, Lukás
    Brno Univ Technol, Brno, Czech Republic.
    Parameterized verification through view abstraction2016In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, 495-516 p.Article in journal (Refereed)
    Abstract [en]

    We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

  • 13.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Haziza, Frédéric
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Holík, Lukás
    Block me if you can!: Context-sensitive parameterized verification2014In: Static Analysis: SAS 2014, Springer, 2014, 1-17 p.Conference paper (Refereed)
    Abstract [en]

    We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

  • 14.
    Abdulla, Parosh Aziz
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Haziza, Frédéric
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Holík, Lukáš
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    All for the price of few: (Parameterized verification through view abstraction)2013In: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2013, 476-495 p.Conference paper (Refereed)
  • 15.
    Abdulla, Parosh
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Trinh, Cong Quy
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Automated Verification of Linearization Policies2016In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Conference paper (Other academic)
    Abstract [en]

    We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

  • 16.
    Atig, Mohamed Faouzi
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Saivasan, Prakash
    Chennai Mathematical Institute, Chennai.
    On Bounded Reachability Analysis of Shared Memory Systems2014In: {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014, New Delhi, India, 2014Conference paper (Refereed)
  • 17.
    Atig, Mohamed Faouzi
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Bouajjani, Ahmed
    LIAFA, CNRS and University of Paris Diderot.
    Parlato, Gennaro
    University of Southampton.
    Context-Bounded Analysis of TSO Systems2014In: From Programs to Systems: The Systems perspective in Computing / [ed] Bensalem, S; Lakhneck, Y; Legay, A, Springer, 2014, 21-38 p.Conference paper (Other academic)
    Abstract [en]

    We address the state reachability problem in concurrent programs running over the TSO weak memory model. This problem has been shown to be decidable with non-primitive recursive complexity in the case of finite-state threads. For recursive threads this problem is undecidable. The aim of this paper is to provide under-approximate analyses for TSO systems that are decidable and have better (elementary) complexity. We propose three bounding concepts for TSO behaviors that are inspired from the concept of bounding the number of context switches introduced by Qadeer and Rehof for the sequentially consistent (SC) model. We investigate the decidability and the complexity of the state reachability problems under these three bounding concepts for TSO, and provide reduction of these problems to known reachability problems of concurrent systems under the SC semantics.

  • 18.
    Atig, Mohamed Faouzi
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kumar, K. Narayan
    Saivasan, Prakash
    Acceleration in Multi-PushDown Systems2016In: Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2016, 698-714 p.Conference paper (Refereed)
  • 19.
    Ayyalasomayajula, Kalyan Ram
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Visual Information and Interaction. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Brun, Anders
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Visual Information and Interaction. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computerized Image Analysis and Human-Computer Interaction.
    Document binarization using topological clustering guided Laplacian Energy Segmentation2014In: Proceedings International Conference on Frontiers in Handwriting Recognition (ICFHR), 2014, 2014, 523-528 p.Conference paper (Refereed)
    Abstract [en]

    The current approach for text binarization proposesa clustering algorithm as a preprocessing stage toan energy-based segmentation method. It uses a clusteringalgorithm to obtain a coarse estimate of the background (BG)and foreground (FG) pixels. These estimates are used as a priorfor the source and sink points of a graph cut implementation,which is used to efficiently find the minimum energy solution ofan objective function to separate the BG and FG. The binaryimage thus obtained is used to refine the edge map that guidesthe graph cut algorithm. A final binary image is obtained byonce again performing the graph cut guided by the refinededges on a Laplacian of the image.

  • 20.
    Bachelder, Steven
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Hayashi, Masaki
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Nakajima, Masayuki
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    4K/8K Ultra High-resolution Interactive Display System for Museum Collections: Providing Information and Context2013Conference paper (Other academic)
  • 21.
    Bachelder, Steven
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Ohta, Takashi
    Tokyo University of Technology.
    Nakajima, Masayuki
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Hayashi, Masaki
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Kondo, Kunio
    Tokyo University of Technology.
    Andreasson, Joakim
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Böstrom, Pelle
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Khatib, Youssef
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Lau, Kakee
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Lewis, Jonas
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Arts, Department of Game Design.
    Research Work-Package Methodology exemplified by the Multiple Screens Project: Pinch Game using Unity for Android2013Conference paper (Other academic)
  • 22.
    Badiozamany, Sobhan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
    Real-time data stream clustering over sliding windows2016Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    In many applications, e.g. urban traffic monitoring, stock trading, and industrial sensor data monitoring, clustering algorithms are applied on data streams in real-time to find current patterns. Here, sliding windows are commonly used as they capture concept drift.

    Real-time clustering over sliding windows is early detection of continuously evolving clusters as soon as they occur in the stream, which requires efficient maintenance of cluster memberships that change as windows slide.

    Data stream management systems (DSMSs) provide high-level query languages for searching and analyzing streaming data. In this thesis we extend a DSMS with a real-time data stream clustering framework called Generic 2-phase Continuous Summarization framework (G2CS).  G2CS modularizes data stream clustering by taking as input clustering algorithms which are expressed in terms of a number of functions and indexing structures. G2CS supports real-time clustering by efficient window sliding mechanism and algorithm transparent indexing. A particular challenge for real-time detection of a high number of rapidly evolving clusters is efficiency of window slides for clustering algorithms where deletion of expired data is not supported, e.g. BIRCH. To that end, G2CS includes a novel window maintenance mechanism called Sliding Binary Merge (SBM). To further improve real-time sliding performance, G2CS uses generation-based multi-dimensional indexing where indexing structures suitable for the clustering algorithms can be plugged-in.

    List of papers
    1. Scalable ordered indexing of streaming data
    Open this publication in new window or tab >>Scalable ordered indexing of streaming data
    2012 (English)In: 3rd International Workshop on Accelerating Data Management Systems using Modern Processor and Storage Architectures, 2012, 11- p.Conference paper, Published paper (Refereed)
    National Category
    Computer Science
    Identifiers
    urn:nbn:se:uu:diva-185068 (URN)
    Conference
    ADMS 2012, Istanbul, Turkey
    Projects
    eSSENCE
    Available from: 2012-08-27 Created: 2012-11-19 Last updated: 2016-09-09Bibliographically approved
    2. Grand challenge: Implementation by frequently emitting parallel windows and user-defined aggregate functions
    Open this publication in new window or tab >>Grand challenge: Implementation by frequently emitting parallel windows and user-defined aggregate functions
    Show others...
    2013 (English)In: Proc. 7th ACM International Conference on Distributed Event-Based Systems, New York: ACM Press, 2013, 325-330 p.Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    New York: ACM Press, 2013
    National Category
    Computer Science
    Identifiers
    urn:nbn:se:uu:diva-211954 (URN)10.1145/2488222.2488284 (DOI)978-1-4503-1758-0 (ISBN)
    External cooperation:
    Conference
    DEBS 2013
    Available from: 2013-06-29 Created: 2013-12-03 Last updated: 2016-09-09Bibliographically approved
    3. Distributed multi-query optimization of continuous clustering queries
    Open this publication in new window or tab >>Distributed multi-query optimization of continuous clustering queries
    2014 (English)In: Proc. VLDB 2014 PhD Workshop, 2014Conference paper, Published paper (Refereed)
    Abstract [en]

    This work addresses the problem of sharing execution plans for queries that continuously cluster streaming data to provide an evolving summary of the data stream. This is challenging since clustering is an expensive task, there might be many clustering queries running simultaneously, each continuous query has a long life time span, and the execution plans often overlap. Clustering is similar to conventional grouped aggregation but cluster formation is more expensive than group formation, which makes incremental maintenance more challenging. The goal of this work is to minimize response time of continuous clustering queries with limited resources through multi-query optimization. To that end, strategies for sharing execution plans between continuous clustering queries are investigated and the architecture of a system is outlined that optimizes the processing of multiple such queries. Since there are many clustering algorithms, the system should be extensible to easily incorporate user defined clustering algorithms.

    National Category
    Computer Science
    Research subject
    Computer Science with specialization in Database Technology
    Identifiers
    urn:nbn:se:uu:diva-302790 (URN)
    External cooperation:
    Conference
    VLDB 2014
    Available from: 2016-09-09 Created: 2016-09-09 Last updated: 2016-09-09Bibliographically approved
    4. Framework for real-time clustering over sliding windows
    Open this publication in new window or tab >>Framework for real-time clustering over sliding windows
    2016 (English)In: Proc. 28th International Conference on Scientific and Statistical Database Management, New York: ACM Press, 2016, 1-13 p., 19Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    New York: ACM Press, 2016
    National Category
    Computer Science
    Identifiers
    urn:nbn:se:uu:diva-302792 (URN)10.1145/2949689.2949696 (DOI)978-1-4503-4215-5 (ISBN)
    External cooperation:
    Conference
    SSDBM 2016
    Available from: 2016-07-18 Created: 2016-09-09 Last updated: 2016-09-12Bibliographically approved
  • 23. Baird, Ryan
    et al.
    Gavin, Peter
    Själander, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Whalley, David
    Uh, Gang-Ryung
    Optimizing transfers of control in the static pipeline architecture2015In: Proc. 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, New York: ACM Press, 2015, 7-16 p.Conference paper (Refereed)
    Abstract [en]

    Statically pipelined processors offer a new way to improve the performance beyond that of a traditional in-order pipeline while simultaneously reducing energy usage by enabling the compiler to control more fine-grained details of the program execution. This paper describes how a compiler can exploit the features of the static pipeline architecture to apply optimizations on transfers of control that are not possible on a conventional architecture. The optimizations presented in this paper include hoisting the target address calculations for branches, jumps, and calls out of loops, performing branch chaining between calls and jumps, hoisting the setting of return addresses out of loops, and exploiting conditional calls and returns. The benefits of performing these transfer of control optimizations include a 6.8% reduction in execution time and a 3.6% decrease in estimated energy usage.

  • 24. Bardizbanyan, Alen
    et al.
    Själander, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Whalley, David
    Larsson-Edefors, Per
    Improving data access efficiency by using context-aware loads and stores2015In: Proc. 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, New York: ACM Press, 2015, 27-36 p.Conference paper (Refereed)
    Abstract [en]

    Memory operations have a significant impact on both performance and energy usage even when an access hits in the level-one data cache (L1 DC). Load instructions in particular affect performance as they frequently result in stalls since the register to be loaded is often referenced before the data is available in the pipeline. L1 DC accesses also impact energy usage as they typically require significantly more energy than a register file access. Despite their impact on performance and energy usage, L1 DC accesses on most processors are performed in a general fashion without regard to the context in which the load or store operation is performed. We describe a set of techniques where the compiler enhances load and store instructions so that they can be executed with fewer stalls and/or enable the L1 DC to be accessed in a more energy-efficient manner. We show that using these techniques can simultaneously achieve a 6% gain in performance and a 43% reduction in L1 DC energy usage.

  • 25. Basirat, Ali
    et al.
    Faili, Heshaam
    Bridge the gap between statistical and hand-crafted grammars2013In: Computer speech & language (Print), ISSN 0885-2308, E-ISSN 1095-8363, Vol. 27, no 5, 1085-1104 p.Article in journal (Refereed)
    Abstract [en]

    LTAG is a rich formalism for performing NLP tasks such as semantic interpretation, parsing, machine translation and information retrieval. Depend on the specific NLP task, different kinds of LTAGs for a language may be developed. Each of these LTAGs is enriched with some specific features such as semantic representation and statistical information that make them suitable to be used in that task. The distribution of these capabilities among the LTAGs makes it difficult to get the benefit from all of them in NLP applications.

    This paper discusses a statistical model to bridge between two kinds LTAGs for a natural language in order to benefit from the capabilities of both kinds. To do so, an HMM was trained that links an elementary tree sequence of a source LTAG onto an elementary tree sequence of a target LTAG. Training was performed by using the standard HMM training algorithm called Baum–Welch. To lead the training algorithm to a better solution, the initial state of the HMM was also trained by a novel EM-based semi-supervised bootstrapping algorithm.

    The model was tested on two English LTAGs, XTAG (XTAG-Group, 2001) and MICA's grammar (Bangalore et al., 2009) as the target and source LTAGs, respectively. The empirical results confirm that the model can provide a satisfactory way for linking these LTAGs to share their capabilities together.

  • 26.
    Basirat, Ali
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Languages, Department of Linguistics and Philology.
    Nivre, Joakim
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Languages, Department of Linguistics and Philology.
    Greedy Universal Dependency Parsing with Right Singular Word Vectors2016Conference paper (Refereed)
    Abstract [en]

    A set of continuous feature vectors formed by right singular vectors of a transformed co-occurrence matrix are used with the Stanford neural dependency parser to train parsing models for a limited number of languages in the corpus of universal dependencies. We show that the feature vector can help the parser to remain greedy and be as accurate as (or even more accurate than) some other greedy and non-greedy parsers.

  • 27.
    Benaceur, Amel
    et al.
    INRIA Rocquencourt.
    Chilton, Chris
    University of Oxford.
    Isberner, Malte
    Technical University of Dortmund.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Automated Mediator Synthesis: Combining Behavioural and Ontological Reasoning2013In: SEFM 2013, 11th Int. Conf. on Software Engineering and Formal Methods / [ed] Robert M. Hierons, Mercedes G. Merayo, Mario Bravetti, Springer, 2013, 274-288 p.Conference paper (Refereed)
    Abstract [en]

    Software systems are increasingly composed of independentlydeveloped heterogeneous components. To ensure interoperability, medi-ators are needed that coordinate actions and translate exchanged mes-sages between the components. We present a technique for automatedsynthesis of mediators, by means of a quotient operator, that is based onbehavioural models of the components and an ontological model of thedata domain. By not requiring a specification of the composed system,the method supports both off-line and run-time synthesis. The obtainedmediator is the most general component that ensures freedom of bothcommunication mismatches and deadlock in the composition. Validationof the approach is given by implementation of a prototype tool, while ap-plicability is illustrated on heterogeneous holiday booking components.

  • 28.
    Berglund, Anders
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Understanding Network Protocols. A Phenomenographic study: Invited seminar at the 2nd Annual Finnish/Baltic Sea Conference on Computer Science Education2002Other (Other academic)
    Abstract [en]

    How students who participate in a project-centered, internationally distributed, university course in computer systems taught jointly by two universities understand a network protocol, TCP, is described in this paper. Insights into students' understanding are gained through an empirical phenomenographic research approach. The use of phenomenography as a research approach makes it possible to learn about computer science, as it is experienced by the students. Some aspects that indicate good learning outcomes are identified, such as being capable of understanding a protocol in different ways and of making relevant choices between the ways it could be experienced according to the context in which it appears. Based on these results a discussion on learning and teaching is developed.

  • 29.
    Berglund, Anders
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Sundin, Peter
    Uppsala University, Disciplinary Domain of Science and Technology, För teknisk-naturvetenskapliga fakulteten gemensamma enheter, International Science Programme (ISP).
    The Development of Cooperation Between Al Baha University and Uppsala University, Sweden2014In: International Exhibition and Conference on Higher Education, Riyadh, Saudi Arabia, 2014Conference paper (Other academic)
    Abstract [en]

    Developing new master level education is a complex task. Not only is the competence within the discipline crucial; teaching and as a consequence, learning, must also be research-focused and must aim to encourage the students to develop into independent scholars.

    In this collaborative, multi-facetted project Al Baha University, Saudi Arabia, (ABU) and Uppsala University, Sweden, (UU) work jointly to develop ABU into a leading actor in master level education with a corresponding research profile. The schools/departments take their own decisions on design and priorities of the activities. In this way the project profits from the local competencies at both sites and becomes locally situated and thus closer to the needs and expectations of the ABU staff.

    The partners entered into collaboration 2011. Among initial achievements was the common identification of the need of a bridging year for tentative master’s students, to complement the skills from the undergraduate (UG) level, and reinforce the command of English, which is a necessary tool in international education. In addition, computer science and mathematics were selected as the initial development areas.

    Within mathematics, the Department of Mathematics at UU was engaged in a discussion aiming primarily to develop the UG curriculum to match the needs of a future master programme, and secondly to develop the curriculum of a ABU master programme in mathematics to match UU standards, with the possibility in mind of student exchange targeting specific courses and thesis studies.

    Meanwhile, in the autumn 2013 a female staff member of ABU was admitted as PhD student in mathematics at UU, and has now started her second semester of full time studies.

    Within computer science (CS), the project tackles the significant challenges to encourage students, teachers and the formal university structures to embrace the ideas of Scholarship of Teaching and Learning (SoTL). The aim is to promote staff and students to broaden their perspective on what research and investigation means and to critically examine teaching and learning. As a consequence, the ways to relate to the students, the subject area, the teaching and the colleagues must be scrutinised, with the intent of finding new teaching and learning forms.

    The project implements these ideas in several ways. Currently a staff development course is given as a starting point for the project within CS. With a focus on the changes needed to implement the ideas of SoTL, the course participants make their own pedagogical development projects, and study their own practice and its outcomes using rigorous research-based methods. As a continuation, during the coming years, the two universities will run a set of workshops, mainly with a methodological focus, followed by a series of three conferences, with the first one serving the local area, and the last being an internationally recognised Institute of Electrical and Electronics Engineers (IEEE) sponsored conference. 

  • 30.
    Berglund, Emil
    et al.
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Social Sciences, Department of Informatics and Media.
    Facklam, Alexander
    Uppsala University, Disciplinary Domain of Humanities and Social Sciences, Faculty of Social Sciences, Department of Informatics and Media.
    Framgång eller förfall?: Utvecklingen, riskerna och potentialen av BYOD2016Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
    Abstract [sv]

    Uppsatsen undersöker fenomenet Bring Your Own Device (BYOD), dess för- och nackdelar samt hur riskerna BYOD medför kan hanteras. För att uppnå detta har en litteraturstudie genomförts. Denna kompletteras av en enkätstudie på Stockholms Läns Landsting och tre intervjuer på Uppsala Kommun med målet att se hur dessa organisationer hanterar BYOD. Arbetet ger en djup insikt i BYOD olika aspekter och visar även på hur de risker som uppkommer kan hanteras.

  • 31.
    Bischoff, Sascha
    et al.
    University of Southampton, Southampton, UK.
    Sandberg, Andreas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Hansson, Andreas
    ARM, Cambridge, UK.
    Dam, Sunwoo
    ARM, Austin, TX, USA.
    Saidi, Ali
    ARM, Austin, TX, USA.
    Horsnell, Matthew
    ARM, Cambridge, UK.
    Al-Hashimi, Bashir
    University of Southampton, Southampton, UK.
    Flexible and High-Speed System-Level Performance Analysis using Hardware-Accelerated Simulation2013Conference paper (Other academic)
  • 32.
    Bollig, Benedikt
    et al.
    LSV, ENS Cachan.
    Cyriac, Aiswarya
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Gastin, Paul
    LSV, ENS Cachan.
    Zeitoun, Marc
    University of Bordeaux.
    Temporal logics for concurrent recursive programs: Satisfiability and model checking2014In: Journal of Applied Logic, ISSN 1570-8683, E-ISSN 1570-8691, Vol. 12, no 4, 395-416 p.Article in journal (Refereed)
  • 33.
    Boström, Carl
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Herelius, Johan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Hugosson, Mathias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Maleev, Sergej
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
    Automatic reading and interpretation of paper invoices: ADC invoice2016Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
    Abstract [en]

    Manually typing long numbers on paper invoices is tedious and timeconsuming work. The task of typing all the fields of an invoice into a text editor was given to two subjects working with bookkeeping, and the average time consumed was measured to be five minutes. The time and cost spent on manual typing will accumulate for companies that receive a lot of invoices. Swedbank along with other banks, have addressed this issue with a mobile application that reads and interprets the numbers on an invoice using the built in camera. This solution is directed to the public and the extracted information cannot be imported into bookkeeping software. A standalone software for digital reading and interpretation of scanned invoices is our solution for companies in regards to this issue.

    There is already technology available that will interpret written text. These techniques were applied in our work, but the focus of this project was to implement algorithms for finding the location for a specific number and resolve what bookkeeping terms the number references e.g. OCR, IBAN numbers, etc. This is hampered by the missing of a general invoice layout.

    52% of all the sought information was extracted correctly and almost 95% of the bookkeeping details that are changed most frequently on invoices from the same service providers were extracted correctly. The average time it takes for the application to extract the vital data is 30-40 seconds.

  • 34.
    Ceballos, Germán
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Black-Schaffer, David
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Shared Resource Sensitivity in Task-Based Runtime Systems2013In: Proceedings of the 6th Swedish Workshop on Multi-Core Computing, Halmstad, Sweden: Halmstad University , 2013Conference paper (Refereed)
    Abstract [en]

    Task-based programming methodologies have become a popular alternative to explicit threading because they leave most of the complexity of scheduling and load balancing to the runtime system. Modern task schedulers use task execution information to build models which they can then use to predict future task performance and produce better schedules. However, while shared resource sensitivity, such as the use of shared cache, is widely known to hurt performance, current schedulers do not address this in their scheduling.This work applies low-overhead techniques for measuring resource sensitivity to task-based runtime systems to profile individual task behavior.We present results for several benchmarks, both in an isolated environment (all resources available) and in normal contention scenarios, and establish a direct quantitative cor-relation between individual tasks and the entire application sensitivity.We present insight into areas where these profiling techniques could enable significant gains in performance due to better scheduling, and conclude what scenarios are necessary for such improvements.

  • 35.
    Chen, Taolue
    et al.
    University of Oxford.
    Chilton, Chris
    University of Oxford.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kwiatkowska, Marta
    University of Oxford.
    A Compositional Specification Theory for Component Behaviours2012Report (Other academic)
  • 36.
    Chilton, Chris
    et al.
    University of Oxford.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kwiatkowska, Marta
    University of Oxford.
    An Algebraic Theory of Interface Automata2013Report (Other academic)
  • 37.
    Chilton, Chris
    et al.
    University of Oxford.
    Jonsson, Bengt
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kwiatkowska, Marta
    University of Oxford.
    Assume-Guarantee Reasoning for Safe Component Behaviours2012In: Proc. FACS: Formal Aspects of Component Software, 9th Int. Symp. / [ed] Corina S. Pasareanu, Gwen Salaün, Springer, 2012, 92-109 p.Conference paper (Refereed)
    Abstract [en]

    We formulate a sound and complete assume-guarantee framework for reasoning compositionally about safety properties of component behaviours. The specification of a component, which constrains the temporal ordering of input and output interactions with the environment, is expressed in terms of two prefix-closed sets of traces: an assumption and guarantee. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated by considering a simple printing example.

  • 38.
    Cyriac, Aiswarya
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Gastin, Paul
    LSV, ENS Cachan.
    Reasoning about distributed systems: WYSIWYG2014Conference paper (Refereed)
  • 39.
    Cyriac, Aiswarya
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Gastin, Paul
    LSV, ENS Cachan.
    Narayan Kumar, K.
    Chennai Mathematical Institute.
    Controllers for the Verification of Communicating Multi-Pushdown Systems2014Conference paper (Refereed)
  • 40.
    Cyriac, Aiswarya
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Gastin, Paul
    Narayan Kumar, K.
    Verifying Communicating Multi-pushdown Systems via Split-Width2014In: Automated Technology for Verification and Analysis, 2014, 1-17 p.Conference paper (Refereed)
    Abstract [en]

    Communicating multi-pushdown systems model networks of multi-threaded recursive programs communicating via reliable FIFO channels. We extend the notion of split-width [8] to this setting, improving and simplifying the earlier definition. Split-width, while having the same power of clique-/tree-width, gives a divide-and-conquer technique to prove the bound of a class, thanks to the two basic operations, shuffle and merge, of the split-width algebra. We illustrate this technique on examples. We also obtain simple, uniform and optimal decision procedures for various verification problems parametrised by split-width.

  • 41.
    Davari, Mahdad
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Advances Towards Data-Race-Free Cache Coherence Through Data Classification2017Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Providing a consistent view of the shared memory based on precise and well-defined semantics—memory consistency model—has been an enabling factor in the widespread acceptance and commercial success of shared-memory architectures. Moreover, cache coherence protocols have been employed by the hardware to remove from the programmers the burden of dealing with the memory inconsistency that emerges in the presence of the private caches. The principle behind all such cache coherence protocols is to guarantee that consistent values are read from the private caches at all times.

    In its most stringent form, a cache coherence protocol eagerly enforces two invariants before each data modification: i) no other core has a copy of the data in its private caches, and ii) all other cores know where to receive the consistent data should they need the data later. Nevertheless, by partly transferring the responsibility for maintaining those invariants to the programmers, commercial multicores have adopted weaker memory consistency models, namely the Total Store Order (TSO), in order to optimize the performance for more common cases.

    Moreover, memory models with more relaxed invariants have been proposed based on the observation that more and more software is written in compliance with the Data-Race-Free (DRF) semantics. The semantics of DRF software can be leveraged by the hardware to infer when data in the private caches might be inconsistent. As a result, hardware ignores the inconsistent data and retrieves the consistent data from the shared memory. DRF semantics therefore removes from the hardware the burden of eagerly enforcing the strong consistency invariants before each data modification. Instead, consistency is guaranteed only when needed. This results in manifold optimizations, such as reducing the energy consumption and improving the performance and scalability. The efficiency of detecting and discarding the inconsistent data is an important factor affecting the efficiency of such coherence protocols. For instance, discarding the consistent data does not affect the correctness, but results in performance loss and increased energy consumption.

    In this thesis we show how data classification can be leveraged as an effective tool to simplify the cache coherence based on the DRF semantics. In particular, we introduce simple but efficient hardware-based private/shared data classification techniques that can be used to efficiently detect the inconsistent data, thus enabling low-overhead and scalable cache coherence solutions based on the DRF semantics.

    List of papers
    1. Hierarchical private/shared classification: The key to simple and efficient coherence for clustered cache hierarchies
    Open this publication in new window or tab >>Hierarchical private/shared classification: The key to simple and efficient coherence for clustered cache hierarchies
    2015 (English)In: Proc. 21st International Symposium on High Performance Computer Architecture, IEEE Computer Society Digital Library, 2015, 186-197 p.Conference paper, Published paper (Refereed)
    Abstract [en]

    Hierarchical clustered cache designs are becoming an appealing alternative for multicores. Grouping cores and their caches in clusters reduces network congestion by localizing traffic among several hierarchical levels, potentially enabling much higher scalability. While such architectures can be formed recursively by replicating a base design pattern, keeping the whole hierarchy coherent requires more effort and consideration. The reason is that, in hierarchical coherence, even basic operations must be recursive. As a consequence, intermediate-level caches behave both as directories and as leaf caches. This leads to an explosion of states, protocol-races, and protocol complexity. While there have been previous efforts to extend directory-based coherence to hierarchical designs their increased complexity and verification cost is a serious impediment to their adoption. We aim to address these concerns by encapsulating all hierarchical complexity in a simple function: that of determining when a data block is shared entirely within a cluster (sub-tree of the hierarchy) and is private from the outside. This allows us to eliminate complex recursive operations that span the hierarchy and instead employ simple coherence mechanisms such as self-invalidation and write-through-now restricted to operate within the cluster where a data block is shared. We examine two inclusivity options and discuss the relation of our approach to the recently proposed Hierarchical-Race-Free (HRF) memory models. Finally, comparisons to a hierarchical directory-based MOESI, VIPS-M, and TokenCMP protocols show that, despite its simplicity our approach results in competitive performance and decreased network traffic.

    Place, publisher, year, edition, pages
    IEEE Computer Society Digital Library, 2015
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-265651 (URN)10.1109/HPCA.2015.7056032 (DOI)000380564900016 ()9781479989300 (ISBN)
    External cooperation:
    Conference
    HPCA 2015, February 7–11, Burlingame, CA
    Available from: 2015-02-11 Created: 2015-11-02 Last updated: 2017-04-22Bibliographically approved
    2. The effects of granularity and adaptivity on private/shared classification for coherence
    Open this publication in new window or tab >>The effects of granularity and adaptivity on private/shared classification for coherence
    2015 (English)In: ACM Transactions on Architecture and Code Optimization (TACO), ISSN 1544-3566, E-ISSN 1544-3973, Vol. 12, no 3, 26Article in journal (Refereed) Published
    Abstract [en]

    Classification of data into private and shared has proven to be a catalyst for techniques to reduce coherence cost, since private data can be taken out of coherence and resources can be concentrated on providing coherence for shared data. In this article, we examine how granularity-page-level versus cache-line level- and adaptivity-going from shared to private-affect the outcome of classification and its final impact on coherence. We create a classification technique, called Generational Classification, and a coherence protocol called Generational Coherence, which treats data as private or shared based on cache-line generations. We compare two coherence protocols based on self-invalidation/self-downgrade with respect to data classification. Our findings are enlightening: (i) Some programs benefit from finer granularity, some benefit further from adaptivity, but some do not benefit from either. (ii) Reducing the amount of shared data has no perceptible impact on coherence misses caused by self-invalidation of shared data, hence no impact on performance. (iii) In contrast, classifying more data as private has implications for protocols that employ write-through as a means of self-downgrade, resulting in network traffic reduction-up to 30%-by reducing write-through traffic.

    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-265580 (URN)10.1145/2790301 (DOI)000363004100001 ()
    Available from: 2015-10-06 Created: 2015-11-02 Last updated: 2017-04-22Bibliographically approved
    3. An efficient, self-contained, on-chip directory: DIR1-SISD
    Open this publication in new window or tab >>An efficient, self-contained, on-chip directory: DIR1-SISD
    2015 (English)In: Proc. 24th International Conference on Parallel Architectures and Compilation Techniques, IEEE Computer Society, 2015, 317-330 p.Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    IEEE Computer Society, 2015
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-265611 (URN)10.1109/PACT.2015.23 (DOI)000378942700027 ()978-1-4673-9524-3 (ISBN)
    Conference
    PACT 2015, October 18–21, San Francisco, CA
    Available from: 2015-11-02 Created: 2015-11-02 Last updated: 2017-04-22Bibliographically approved
    4. Scope-Aware Classification: Taking the hierarchical private/shared data classification to the next level
    Open this publication in new window or tab >>Scope-Aware Classification: Taking the hierarchical private/shared data classification to the next level
    2017 (English)Report (Other academic)
    Series
    Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2017-008
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-320324 (URN)
    Available from: 2017-04-27 Created: 2017-04-19 Last updated: 2017-07-03Bibliographically approved
    5. The best of both works: A hybrid data-race-free cache coherence scheme
    Open this publication in new window or tab >>The best of both works: A hybrid data-race-free cache coherence scheme
    2017 (English)In: ACM Transactions on Architecture and Code Optimization (TACO), ISSN 1544-3566, E-ISSN 1544-3973, Vol. 14Article in journal (Refereed) Accepted
    National Category
    Computer Systems
    Identifiers
    urn:nbn:se:uu:diva-320320 (URN)
    Available from: 2017-04-19 Created: 2017-04-19 Last updated: 2017-07-03Bibliographically approved
  • 42.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    The best of both works: A hybrid data-race-free cache coherence scheme2017In: ACM Transactions on Architecture and Code Optimization (TACO), ISSN 1544-3566, E-ISSN 1544-3973, Vol. 14Article in journal (Refereed)
  • 43.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Scope-Aware Classification: Taking the hierarchical private/shared data classification to the next level2017Report (Other academic)
  • 44.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Ros, Alberto
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    The effects of granularity and adaptivity on private/shared classification for coherence2015In: ACM Transactions on Architecture and Code Optimization (TACO), ISSN 1544-3566, E-ISSN 1544-3973, Vol. 12, no 3, 26Article in journal (Refereed)
    Abstract [en]

    Classification of data into private and shared has proven to be a catalyst for techniques to reduce coherence cost, since private data can be taken out of coherence and resources can be concentrated on providing coherence for shared data. In this article, we examine how granularity-page-level versus cache-line level- and adaptivity-going from shared to private-affect the outcome of classification and its final impact on coherence. We create a classification technique, called Generational Classification, and a coherence protocol called Generational Coherence, which treats data as private or shared based on cache-line generations. We compare two coherence protocols based on self-invalidation/self-downgrade with respect to data classification. Our findings are enlightening: (i) Some programs benefit from finer granularity, some benefit further from adaptivity, but some do not benefit from either. (ii) Reducing the amount of shared data has no perceptible impact on coherence misses caused by self-invalidation of shared data, hence no impact on performance. (iii) In contrast, classifying more data as private has implications for protocols that employ write-through as a means of self-downgrade, resulting in network traffic reduction-up to 30%-by reducing write-through traffic.

  • 45.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Ros, Alberto
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    An efficient, self-contained, on-chip directory: DIR1-SISD2015In: Proc. 24th International Conference on Parallel Architectures and Compilation Techniques, IEEE Computer Society, 2015, 317-330 p.Conference paper (Refereed)
  • 46.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Ros, Alberto
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    The Effects of Granularity and Adaptivity on Private/Shared Classification for Coherence2014Conference paper (Refereed)
  • 47.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Ros, Alberto
    Hagersten, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Effects of Granularity/Adaptivity on Private/Shared Classification for Coherence2015Conference paper (Other academic)
  • 48.
    Davari, Mahdad
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Ros, Alberto
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Kaxiras, Stefanos
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    System and method for data classification and efficient virtual cache coherence without reverse translation2013Patent (Other (popular science, discussion, etc.))
    Abstract [en]

    An on-chip memory hierarchy organization for a multicore processing system is disclosed. The hierarchy supports virtual- addressed private caches and a physical-addressed shared cache. The hierarchy classifies cache line data as private or shared to support a one-directional request response protocol. The classification can be determined from the generational behavior of a cache line in the private caches. Cache lines having a single generation in a private cache are Private, and cache lines having overlapping generations in two or more private caches are Shared. The Private or Shared classification is performed dynamically at run-time in hardware using a single translation lookaside buffer at the interface between the private and shared caches. The coherence protocol uses the data classification in a dynamic write policy for both shared data race free data and private data, differentiating in when data is put back to the shared cache based on the classification.

  • 49. Davis, Brandon
    et al.
    Baird, Ryan
    Gavin, Peter
    Själander, Magnus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Finlayson, Ian
    Rasapour, Farhad
    Cook, Gregory
    Uh, Gang-Ryung
    Whalley, David
    Tyson, Gary
    Scheduling instruction effects for a statically pipelined processor2015In: Proc. International Conference on Compilers, Architectures, and Synthesis for Embedded Systems: CASES 2015, Piscataway, NJ: IEEE Press, 2015, 167-176 p.Conference paper (Refereed)
    Abstract [en]

    Statically pipelined processors have a fully exposed datapath where all portions of the pipeline are directly controlled by effects within an instruction, which simplifies hardware and enables a new level of compiler optimizations. This paper describes an effect scheduling strategy to aggressively compact instructions, which has a critical impact on code size and performance. Unique scheduling challenges include more frequent name dependences and fewer renaming opportunities due to static pipeline (SP) registers being dedicated for specific operations. We also realized the SP in a hardware implementation language (VHDL) to evaluate the real energy bene fits. Despite the compiler challenges, we achieve performance, code size, and energy improvements compared to a conventional MIPS processor.

  • 50.
    De Guglielmo, Domenico
    et al.
    Univ. of Pisa.
    Al Nahas, Beshr
    SICS.
    Duquennoy, Simon
    SICS.
    Voigt, Thiemo
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication. SICS, S-16429 Kista, Sweden.
    Anastasi, Giuseppe
    University of Pisa.
    Analysis and experimental evaluation of IEEE 802.15.4e TSCH CSMA-CA Algorithm2017In: IEEE Transactions on Vehicular Technology, ISSN 0018-9545, E-ISSN 1939-9359, Vol. 66, no 2, 1573-1588 p.Article in journal (Refereed)
    Abstract [en]

    Time-slotted channel hopping (TSCH) is one of the medium access control (MAC) behavior modes defined in the IEEE 802.15.4e standard. It combines time-slotted access and channel hopping, thus providing predictable latency, energy efficiency, communication reliability, and high network capacity. TSCH provides both dedicated and shared links. The latter is special slots assigned to more than one transmitter, whose concurrent access is regulated by a carrier-sense multiple access with collision avoidance (CSMA-CA) algorithm. In this paper, we develop an analytical model of the TSCH CSMA-CA algorithm to predict the performance experienced by nodes when using shared links. The model allows for deriving a number of metrics, such as delivery probability, packet latency, and energy consumption of nodes. Moreover, it considers the capture effect (CE) that typically occurs in real wireless networks. We validate the model through simulation experiments and measurements in a real testbed. Our results show that the model is very accurate. Furthermore, we found that the CE plays a fundamental role as it can significantly improve the performance experienced by nodes.

1234 1 - 50 of 176
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf