From non-preemptive to preemptive scheduling using synchronization synthesis

DOI10.1007/S10703-016-0256-5MaRDI QIDQ5892421zbMATH OpenOpenAlexWikidataFDO

Authors Pavol Černý, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach, Edmund Clarke, Thomas A. Henzinger

Publication date 15 May 2017

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10703-016-0256-5

zbMATH Keywords

concurrencyMAXSATNFA language inclusionsynthesis

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• From non-preemptive to preemptive scheduling using synchronization synthesis
• From preemptive to non-preemptive scheduling using rejections
• From preemptive to non-preemptive speed-scaling scheduling
• From preemptive to non-preemptive speed-scaling scheduling
• Nonpreemptive scheduling of periodic tasks in uni- and multiprocessor systems
• Synthesizing synchronous systems by static scheduling in space-time
• Preemptive Scheduling of Uniform Processor Systems
• The non-preemptive scheduling of periodic tasks upon multiprocessors
• scientific article; zbMATH DE number 1529456
• scientific article; zbMATH DE number 1487943

Cites work

• Abstraction-guided synthesis of synchronization
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Automatic verification of determinism for structured parallel programs
• From non-preemptive to preemptive scheduling using synchronization synthesis
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3986679 (Why is no real title available?)
• scientific article; zbMATH DE number 3765179 (Why is no real title available?)
• Logical Concurrency Control from Sequential Proofs
• Succinct representation of concurrent trace sets
• The notions of consistency and predicate locks in a database system
• Tools and Algorithms for the Construction and Analysis of Systems
• Transactions for software model checking

Cited in

(6)

• Synthesizing synchronous systems by static scheduling in space-time
• Abstract semantic diffing of evolving concurrent programs
• From non-preemptive to preemptive scheduling using synchronization synthesis
• On algorithms verifying initial-and-final-state opacity: complexity, special cases, and comparison
• A game of pawns
• A game of pawns

Describes a project that uses

Uses Software

• CBMC
• Antichains
• Liss
• Limi
• ConRepair
• GitHub

This page was built for publication: From non-preemptive to preemptive scheduling using synchronization synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5892421)