--- _id: '3302' abstract: - lang: eng text: Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler. author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Singh, Anmol id: 72A86902-E99F-11E9-9F62-915534D1B916 last_name: Singh - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.' apa: 'Henzinger, T. A., Singh, A., Singh, V., Wies, T., & Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.' chicago: Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011. ieee: 'T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, 2011, pp. 1–6.' ista: 'Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6.' mla: Henzinger, Thomas A., et al. Static Scheduling in Clouds. USENIX, 2011, pp. 1–6. short: T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6. conference: end_date: 2011-06-15 name: 'HotCloud: Workshop on Hot Topics in Cloud Computing' start_date: 2011-06-14 date_created: 2018-12-11T12:02:33Z date_published: 2011-06-14T00:00:00Z date_updated: 2021-01-12T07:42:31Z day: '14' ddc: - '000' - '005' department: - _id: ToHe file: - access_level: open_access checksum: 21a461ac004bb535c83320fe79b30375 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:14Z date_updated: 2020-07-14T12:46:06Z file_id: '5333' file_name: IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf file_size: 232770 relation: main_file file_date_updated: 2020-07-14T12:46:06Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 1 - 6 publication_status: published publisher: USENIX publist_id: '3338' pubrep_id: '90' quality_controlled: '1' status: public title: Static scheduling in clouds type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3355' abstract: - lang: eng text: Byzantine Fault Tolerant (BFT) protocols aim to improve the reliability of distributed systems. They enable systems to tolerate arbitrary failures in a bounded number of nodes. BFT protocols are usually proven correct for certain safety and liveness properties. However, recent studies have shown that the performance of state-of-the-art BFT protocols decreases drastically in the presence of even a single malicious node. This motivates a formal quantitative analysis of BFT protocols to investigate their performance characteristics under different scenarios. We present HyPerf, a new hybrid methodology based on model checking and simulation techniques for evaluating the performance of BFT protocols. We build a transition system corresponding to a BFT protocol and systematically explore the set of behaviors allowed by the protocol. We associate certain timing information with different operations in the protocol, like cryptographic operations and message transmission. After an elaborate state exploration, we use the time information to evaluate the performance characteristics of the protocol using simulation techniques. We integrate our framework in Mace, a tool for building and verifying distributed systems. We evaluate the performance of PBFT using our framework. We describe two different use-cases of our methodology. For the benign operation of the protocol, we use the time information as random variables to compute the probability distribution of the execution times. In the presence of faults, we estimate the worst-case performance of the protocol for various attacks that can be employed by malicious nodes. Our results show the importance of hybrid techniques in systematically analyzing the performance of large-scale systems. author: - first_name: Raluca full_name: Halalai, Raluca id: 584C6850-E996-11E9-805B-F01764644770 last_name: Halalai - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Halalai R, Henzinger TA, Singh V. Quantitative evaluation of BFT protocols. In: IEEE; 2011:255-264. doi:10.1109/QEST.2011.40' apa: 'Halalai, R., Henzinger, T. A., & Singh, V. (2011). Quantitative evaluation of BFT protocols (pp. 255–264). Presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany: IEEE. https://doi.org/10.1109/QEST.2011.40' chicago: Halalai, Raluca, Thomas A Henzinger, and Vasu Singh. “Quantitative Evaluation of BFT Protocols,” 255–64. IEEE, 2011. https://doi.org/10.1109/QEST.2011.40. ieee: 'R. Halalai, T. A. Henzinger, and V. Singh, “Quantitative evaluation of BFT protocols,” presented at the QEST: Quantitative Evaluation of Systems, Aachen, Germany, 2011, pp. 255–264.' ista: 'Halalai R, Henzinger TA, Singh V. 2011. Quantitative evaluation of BFT protocols. QEST: Quantitative Evaluation of Systems, 255–264.' mla: Halalai, Raluca, et al. Quantitative Evaluation of BFT Protocols. IEEE, 2011, pp. 255–64, doi:10.1109/QEST.2011.40. short: R. Halalai, T.A. Henzinger, V. Singh, in:, IEEE, 2011, pp. 255–264. conference: end_date: 2011-09-08 location: Aachen, Germany name: 'QEST: Quantitative Evaluation of Systems' start_date: 2011-09-05 date_created: 2018-12-11T12:02:51Z date_published: 2011-10-13T00:00:00Z date_updated: 2021-01-12T07:42:53Z day: '13' ddc: - '000' - '004' department: - _id: ToHe doi: 10.1109/QEST.2011.40 file: - access_level: open_access checksum: 4dc8750ab7921f51de992000b13d1b01 content_type: application/pdf creator: system date_created: 2018-12-12T10:07:49Z date_updated: 2020-07-14T12:46:09Z file_id: '4648' file_name: IST-2012-84-v1+1_Quantitative_evaluation_of_BFT_protocols.pdf file_size: 272017 relation: main_file file_date_updated: 2020-07-14T12:46:09Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 255 - 264 publication_status: published publisher: IEEE publist_id: '3260' pubrep_id: '84' quality_controlled: '1' scopus_import: 1 status: public title: Quantitative evaluation of BFT protocols type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3358' abstract: - lang: eng text: The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Singh V, Wies T, Zufferey D. Scheduling large jobs by abstraction refinement. In: ACM; 2011:329-342. doi:10.1145/1966445.1966476' apa: 'Henzinger, T. A., Singh, V., Wies, T., & Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. https://doi.org/10.1145/1966445.1966476' chicago: Henzinger, Thomas A, Vasu Singh, Thomas Wies, and Damien Zufferey. “Scheduling Large Jobs by Abstraction Refinement,” 329–42. ACM, 2011. https://doi.org/10.1145/1966445.1966476. ieee: T. A. Henzinger, V. Singh, T. Wies, and D. Zufferey, “Scheduling large jobs by abstraction refinement,” presented at the EuroSys, Salzburg, Austria, 2011, pp. 329–342. ista: Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342. mla: Henzinger, Thomas A., et al. Scheduling Large Jobs by Abstraction Refinement. ACM, 2011, pp. 329–42, doi:10.1145/1966445.1966476. short: T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342. conference: end_date: 2011-04-13 location: Salzburg, Austria name: EuroSys start_date: 2011-04-10 date_created: 2018-12-11T12:02:53Z date_published: 2011-04-10T00:00:00Z date_updated: 2021-01-12T07:42:55Z day: '10' department: - _id: ToHe doi: 10.1145/1966445.1966476 language: - iso: eng main_file_link: - open_access: '1' url: http://cs.nyu.edu/wies/publ/scheduling_large_jobs_by_abstraction_refinement.pdf month: '04' oa: 1 oa_version: Published Version page: 329 - 342 publication_status: published publisher: ACM publist_id: '3257' quality_controlled: '1' scopus_import: 1 status: public title: Scheduling large jobs by abstraction refinement type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '531' abstract: - lang: eng text: Software transactional memories (STM) are described in the literature with assumptions of sequentially consistent program execution and atomicity of high level operations like read, write, and abort. However, in a realistic setting, processors use relaxed memory models to optimize hardware performance. Moreover, the atomicity of operations depends on the underlying hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We describe RML, a simple language for expressing concurrent programs. We develop a semantics of RML parametrized by a relaxed memory model. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm restricted to two threads and two variables, and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the restricted STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order for two threads and two variables. Finally, we extend the verification results for DSTM and TL2 to an arbitrary number of threads and variables by manually proving that the structural properties of STMs are satisfied at the hardware level of atomicity under the considered relaxed memory models. article_processing_charge: No article_type: original author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: Guerraoui R, Henzinger TA, Singh V. Verification of STM on relaxed memory models. Formal Methods in System Design. 2011;39(3):297-331. doi:10.1007/s10703-011-0131-3 apa: Guerraoui, R., Henzinger, T. A., & Singh, V. (2011). Verification of STM on relaxed memory models. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-011-0131-3 chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Verification of STM on Relaxed Memory Models.” Formal Methods in System Design. Springer, 2011. https://doi.org/10.1007/s10703-011-0131-3. ieee: R. Guerraoui, T. A. Henzinger, and V. Singh, “Verification of STM on relaxed memory models,” Formal Methods in System Design, vol. 39, no. 3. Springer, pp. 297–331, 2011. ista: Guerraoui R, Henzinger TA, Singh V. 2011. Verification of STM on relaxed memory models. Formal Methods in System Design. 39(3), 297–331. mla: Guerraoui, Rachid, et al. “Verification of STM on Relaxed Memory Models.” Formal Methods in System Design, vol. 39, no. 3, Springer, 2011, pp. 297–331, doi:10.1007/s10703-011-0131-3. short: R. Guerraoui, T.A. Henzinger, V. Singh, Formal Methods in System Design 39 (2011) 297–331. date_created: 2018-12-11T11:47:00Z date_published: 2011-12-01T00:00:00Z date_updated: 2021-01-12T08:01:27Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.1007/s10703-011-0131-3 intvolume: ' 39' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://infoscience.epfl.ch/record/178042/files/art3A10.10072Fs10703-011-0131-3.pdf month: '12' oa: 1 oa_version: Published Version page: 297 - 331 publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '7288' quality_controlled: '1' scopus_import: 1 status: public title: Verification of STM on relaxed memory models type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 39 year: '2011' ... --- _id: '3402' abstract: - lang: eng text: Model checking transactional memories (TMs) is difficult because of the unbounded number, length, and delay of concurrent transactions, as well as the unbounded size of the memory. We show that, under certain conditions satisfied by most TMs we know of, the model checking problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several TMs, including two-phase locking, DSTM, and TL2. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the TMs mentioned above. In a first step we show that every TM that enjoys certain structural properties either violates a requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step, we use a model checker to prove the requirement for the TM applied to a most general program with two threads and two variables. In the safety case, the model checker checks language inclusion between two finite-state transition systems, a nondeterministic transition system representing the given TM applied to a most general program, and a deterministic transition system representing a most liberal safe TM applied to the same program. The given TM transition system is nondeterministic because a TM can be used with different contention managers, which resolve conflicts differently. In the liveness case, the model checker analyzes fairness conditions on the given TM transition system. acknowledgement: This research was supported by the Swiss National Science Foundation. This paper is an extended and revised version of our previous work on model checking transactional memories. author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: Guerraoui R, Henzinger TA, Singh V. Model checking transactional memories. Distributed Computing. 2010;22(3):129-145. doi:10.1007/s00446-009-0092-6 apa: Guerraoui, R., Henzinger, T. A., & Singh, V. (2010). Model checking transactional memories. Distributed Computing. Springer. https://doi.org/10.1007/s00446-009-0092-6 chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Model Checking Transactional Memories.” Distributed Computing. Springer, 2010. https://doi.org/10.1007/s00446-009-0092-6. ieee: R. Guerraoui, T. A. Henzinger, and V. Singh, “Model checking transactional memories,” Distributed Computing, vol. 22, no. 3. Springer, pp. 129–145, 2010. ista: Guerraoui R, Henzinger TA, Singh V. 2010. Model checking transactional memories. Distributed Computing. 22(3), 129–145. mla: Guerraoui, Rachid, et al. “Model Checking Transactional Memories.” Distributed Computing, vol. 22, no. 3, Springer, 2010, pp. 129–45, doi:10.1007/s00446-009-0092-6. short: R. Guerraoui, T.A. Henzinger, V. Singh, Distributed Computing 22 (2010) 129–145. date_created: 2018-12-11T12:03:08Z date_published: 2010-03-01T00:00:00Z date_updated: 2021-01-12T07:43:14Z day: '01' doi: 10.1007/s00446-009-0092-6 extern: 1 intvolume: ' 22' issue: '3' main_file_link: - open_access: '0' url: http://infoscience.epfl.ch/record/117513/files/PLDI_paper.pdf month: '03' page: 129 - 145 publication: Distributed Computing publication_status: published publisher: Springer publist_id: '3000' pubrep_id: '74' quality_controlled: 0 status: public title: Model checking transactional memories type: journal_article volume: 22 year: '2010' ... --- _id: '4362' abstract: - lang: eng text: Software transactional memories (STMs) promise simple and efficient concurrent programming. Several correctness properties have been proposed for STMs. Based on a bounded conflict graph algorithm for verifying correctness of STMs, we develop TRACER, a tool for runtime verification of STM implementations. The novelty of TRACER lies in the way it combines coarse and precise runtime analyses to guarantee sound and complete verification in an efficient manner. We implement TRACER in the TL2 STM implementation. We evaluate the performance of TRACER on STAMP benchmarks. While a precise runtime verification technique based on conflict graphs results in an average slowdown of 60x, the two-level approach of TRACER performs complete verification with an average slowdown of around 25x across different benchmarks. alternative_title: - LNCS author: - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Singh V. Runtime verification for software transactional memories. In: Sokolsky O, Rosu G, Tilmann N, et al., eds. Vol 6418. Springer; 2010:421-435. doi:10.1007/978-3-642-16612-9_32' apa: 'Singh, V. (2010). Runtime verification for software transactional memories. In O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner, … G. Pace (Eds.) (Vol. 6418, pp. 421–435). Presented at the RV: International Conference on Runtime Verification, St. Julians, Malta: Springer. https://doi.org/10.1007/978-3-642-16612-9_32' chicago: Singh, Vasu. “Runtime Verification for Software Transactional Memories.” edited by Oleg Sokolsky, Grigore Rosu, Nikolai Tilmann, Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, and Gordon Pace, 6418:421–35. Springer, 2010. https://doi.org/10.1007/978-3-642-16612-9_32. ieee: 'V. Singh, “Runtime verification for software transactional memories,” presented at the RV: International Conference on Runtime Verification, St. Julians, Malta, 2010, vol. 6418, pp. 421–435.' ista: 'Singh V. 2010. Runtime verification for software transactional memories. RV: International Conference on Runtime Verification, LNCS, vol. 6418, 421–435.' mla: Singh, Vasu. Runtime Verification for Software Transactional Memories. Edited by Oleg Sokolsky et al., vol. 6418, Springer, 2010, pp. 421–35, doi:10.1007/978-3-642-16612-9_32. short: V. Singh, in:, O. Sokolsky, G. Rosu, N. Tilmann, H. Barringer, Y. Falcone, B. Finkbeiner, K. Havelund, I. Lee, G. Pace (Eds.), Springer, 2010, pp. 421–435. conference: end_date: 2010-11-04 location: St. Julians, Malta name: 'RV: International Conference on Runtime Verification' start_date: 2010-11-01 date_created: 2018-12-11T12:08:28Z date_published: 2010-01-01T00:00:00Z date_updated: 2021-01-12T07:56:25Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-16612-9_32 editor: - first_name: Oleg full_name: Sokolsky, Oleg last_name: Sokolsky - first_name: Grigore full_name: Rosu, Grigore last_name: Rosu - first_name: Nikolai full_name: Tilmann, Nikolai last_name: Tilmann - first_name: Howard full_name: Barringer, Howard last_name: Barringer - first_name: Ylies full_name: Falcone, Ylies last_name: Falcone - first_name: Bernd full_name: Finkbeiner, Bernd last_name: Finkbeiner - first_name: Klaus full_name: Havelund, Klaus last_name: Havelund - first_name: Insup full_name: Lee, Insup last_name: Lee - first_name: Gordon full_name: Pace, Gordon last_name: Pace intvolume: ' 6418' language: - iso: eng month: '01' oa_version: None page: 421 - 435 publication_status: published publisher: Springer publist_id: '1096' quality_controlled: '1' scopus_import: 1 status: public title: Runtime verification for software transactional memories type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6418 year: '2010' ... --- _id: '4381' abstract: - lang: eng text: Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases. article_processing_charge: No author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Tomar, Anmol id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87 last_name: Tomar - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning of resources in a cloud environment. In: IEEE; 2010:83-90. doi:10.1109/CLOUD.2010.71' apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71' chicago: 'Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,” 83–90. IEEE, 2010. https://doi.org/10.1109/CLOUD.2010.71.' ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE: Flexible provisioning of resources in a cloud environment,” presented at the CLOUD: Cloud Computing, Miami, USA, 2010, pp. 83–90.' ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.' mla: 'Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.' short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90. conference: end_date: 2010-07-10 location: Miami, USA name: 'CLOUD: Cloud Computing' start_date: 2010-07-05 date_created: 2018-12-11T12:08:33Z date_published: 2010-08-26T00:00:00Z date_updated: 2021-01-12T07:56:33Z day: '26' ddc: - '004' department: - _id: ToHe doi: 10.1109/CLOUD.2010.71 file: - access_level: open_access checksum: 98e534675339a8e2beca08890d048145 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:03Z date_updated: 2020-07-14T12:46:28Z file_id: '5188' file_name: IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf file_size: 467436 relation: main_file file_date_updated: 2020-07-14T12:46:28Z has_accepted_license: '1' language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version page: 83 - 90 publication_status: published publisher: IEEE publist_id: '1077' pubrep_id: '47' quality_controlled: '1' scopus_import: 1 status: public title: 'FlexPRICE: Flexible provisioning of resources in a cloud environment' type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2010' ... --- _id: '4382' abstract: - lang: eng text: 'Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to the given underlying memory model. We investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of practical relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows developing more efficient TM implementations.' author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Michal full_name: Kapalka, Michal last_name: Kapalka - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle. In: ACM; 2010:263-272. doi:10.1145/1810479.1810529' apa: 'Guerraoui, R., Henzinger, T. A., Kapalka, M., & Singh, V. (2010). Transactions in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece: ACM. https://doi.org/10.1145/1810479.1810529' chicago: Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh. “Transactions in the Jungle,” 263–72. ACM, 2010. https://doi.org/10.1145/1810479.1810529. ieee: 'R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece, 2010, pp. 263–272.' ista: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.' mla: Guerraoui, Rachid, et al. Transactions in the Jungle. ACM, 2010, pp. 263–72, doi:10.1145/1810479.1810529. short: R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272. conference: end_date: 2010-06-15 location: Santorini, Greece name: 'SPAA: ACM Symposium on Parallel Algorithms and Architectures' start_date: 2010-06-13 date_created: 2018-12-11T12:08:34Z date_published: 2010-06-13T00:00:00Z date_updated: 2021-01-12T07:56:33Z day: '13' ddc: - '005' department: - _id: ToHe doi: 10.1145/1810479.1810529 file: - access_level: open_access checksum: f2ad6c00a6304da34bf21bcdcfd36c4b content_type: application/pdf creator: system date_created: 2018-12-12T10:14:28Z date_updated: 2020-07-14T12:46:28Z file_id: '5080' file_name: IST-2012-46-v1+1_Transactions_in_the_jungle.pdf file_size: 246409 relation: main_file file_date_updated: 2020-07-14T12:46:28Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 263 - 272 publication_status: published publisher: ACM publist_id: '1076' pubrep_id: '46' quality_controlled: '1' status: public title: Transactions in the jungle type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2010' ... --- _id: '4380' abstract: - lang: eng text: Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context. author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Anmol full_name: Tomar, Anmol id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87 last_name: Tomar - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud resources. In: ACM; 2010:1-8. doi:10.1145/1879021.1879022' apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022' chicago: Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “A Marketplace for Cloud Resources,” 1–8. ACM, 2010. https://doi.org/10.1145/1879021.1879022. ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA, 2010, pp. 1–8.' ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.' mla: Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM, 2010, pp. 1–8, doi:10.1145/1879021.1879022. short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8. conference: end_date: 2010-10-29 location: Arizona, USA name: 'EMSOFT: Embedded Software ' start_date: 2010-10-24 date_created: 2018-12-11T12:08:33Z date_published: 2010-10-24T00:00:00Z date_updated: 2021-01-12T07:56:32Z day: '24' ddc: - '005' department: - _id: ToHe doi: 10.1145/1879021.1879022 file: - access_level: open_access checksum: 7680dd24016810710f7c977bc94f85e9 content_type: application/pdf creator: system date_created: 2018-12-12T10:09:42Z date_updated: 2020-07-14T12:46:28Z file_id: '4767' file_name: IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf file_size: 222626 relation: main_file file_date_updated: 2020-07-14T12:46:28Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 1 - 8 publication_status: published publisher: ACM publist_id: '1078' pubrep_id: '48' quality_controlled: '1' scopus_import: 1 status: public title: A marketplace for cloud resources type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2010' ... --- _id: '4395' abstract: - lang: eng text: The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory programs this task is challenging because (1) concurrent threads can observe transformations that would be undetectable in a sequential program, and (2) contemporary multiprocessors commonly use relaxed memory models that complicate the reasoning. In this paper, we present a novel proof methodology for verifying that a local program transformation is sound with respect to a specific hardware memory model, in the sense that it is not observable in any context. The methodology is based on a structural induction and relies on a novel compositional denotational semantics for relaxed memory models that formalizes (1) the behaviors of program fragments as a set of traces, and (2) the effect of memory model relaxations as local trace rewrite operations. To apply this methodology in practice, we implemented a semi- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models. alternative_title: - LNCS author: - first_name: Sebastian full_name: Burckhardt, Sebastian last_name: Burckhardt - first_name: Madanlal full_name: Musuvathi, Madanlal last_name: Musuvathi - first_name: Vasu full_name: Singh, Vasu id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Burckhardt S, Musuvathi M, Singh V. Verifying local transformations on relaxed memory models. In: Gupta R, ed. Vol 6011. Springer; 2010:104-123. doi:10.1007/978-3-642-11970-5_7' apa: 'Burckhardt, S., Musuvathi, M., & Singh, V. (2010). Verifying local transformations on relaxed memory models. In R. Gupta (Ed.) (Vol. 6011, pp. 104–123). Presented at the CC: Compiler Construction, Pahos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-11970-5_7' chicago: Burckhardt, Sebastian, Madanlal Musuvathi, and Vasu Singh. “Verifying Local Transformations on Relaxed Memory Models.” edited by Rajiv Gupta, 6011:104–23. Springer, 2010. https://doi.org/10.1007/978-3-642-11970-5_7. ieee: 'S. Burckhardt, M. Musuvathi, and V. Singh, “Verifying local transformations on relaxed memory models,” presented at the CC: Compiler Construction, Pahos, Cyprus, 2010, vol. 6011, pp. 104–123.' ista: 'Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011, 104–123.' mla: Burckhardt, Sebastian, et al. Verifying Local Transformations on Relaxed Memory Models. Edited by Rajiv Gupta, vol. 6011, Springer, 2010, pp. 104–23, doi:10.1007/978-3-642-11970-5_7. short: S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010, pp. 104–123. conference: end_date: 2010-03-28 location: Pahos, Cyprus name: 'CC: Compiler Construction' start_date: 2010-03-20 date_created: 2018-12-11T12:08:38Z date_published: 2010-04-21T00:00:00Z date_updated: 2021-01-12T07:56:39Z day: '21' doi: 10.1007/978-3-642-11970-5_7 editor: - first_name: Rajiv full_name: Gupta, Rajiv last_name: Gupta extern: '1' intvolume: ' 6011' language: - iso: eng month: '04' oa_version: None page: 104 - 123 publication_status: published publisher: Springer publist_id: '1063' quality_controlled: '1' status: public title: Verifying local transformations on relaxed memory models type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6011 year: '2010' ... --- _id: '4363' author: - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: Singh V. Formalizing and Verifying Transactional Memories. Formalizing and Verifying Transactional Memories. 2009. apa: Singh, V. (2009). Formalizing and Verifying Transactional Memories. Formalizing and Verifying Transactional Memories. EPFL Lausanne. chicago: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing and Verifying Transactional Memories. EPFL Lausanne, 2009. ieee: V. Singh, “Formalizing and Verifying Transactional Memories,” EPFL Lausanne, 2009. ista: Singh V. 2009. Formalizing and Verifying Transactional Memories. EPFL Lausanne. mla: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing and Verifying Transactional Memories, EPFL Lausanne, 2009. short: V. Singh, Formalizing and Verifying Transactional Memories, EPFL Lausanne, 2009. date_created: 2018-12-11T12:08:28Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:25Z day: '01' extern: 1 month: '01' publication: Formalizing and Verifying Transactional Memories publication_status: published publisher: EPFL Lausanne publist_id: '1095' quality_controlled: 0 status: public title: Formalizing and Verifying Transactional Memories type: dissertation year: '2009' ... --- _id: '4383' abstract: - lang: eng text: Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptions are often violated in realistic settings, as STM implementations run on relaxed memory models, with the atomicity of operations as provided by the hardware. This paper presents the first approach to verify STMs under relaxed memory models with atomicity of 32 bit loads and stores, and read-modify-write operations. We present RML, a new high-level language for expressing concurrent algorithms with a hardware-level atomicity of instructions, and whose semantics is parametrized by various relaxed memory models. We then present our tool, FOIL, which takes as input the RML description of an STM algorithm and the description of a memory model, and automatically determines the locations of fences, which if inserted, ensure the correctness of the STM algorithm under the given memory model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of sequential consistency, total store order, partial store order, and relaxed memory order. acknowledgement: This research was supported by the Swiss National Science Foundation. alternative_title: - LNCS author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Guerraoui R, Henzinger TA, Singh V. Software transactional memory on relaxed memory models. In: Vol 5643. Springer; 2009:321-336. doi:10.1007/978-3-642-02658-4_26' apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2009). Software transactional memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_26' chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_26. ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Software transactional memory on relaxed memory models,” presented at the CAV: Computer Aided Verification, 2009, vol. 5643, pp. 321–336.' ista: 'Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336.' mla: Guerraoui, Rachid, et al. Software Transactional Memory on Relaxed Memory Models. Vol. 5643, Springer, 2009, pp. 321–36, doi:10.1007/978-3-642-02658-4_26. short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:34Z date_published: 2009-06-19T00:00:00Z date_updated: 2021-01-12T07:56:34Z day: '19' doi: 10.1007/978-3-642-02658-4_26 extern: 1 file: - access_level: open_access checksum: df3c3e6306afd3f630a9146f91642f0a content_type: application/pdf creator: system date_created: 2018-12-12T10:14:50Z date_updated: 2020-07-14T12:46:28Z file_id: '5105' file_name: IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf file_size: 265763 relation: main_file file_date_updated: 2020-07-14T12:46:28Z intvolume: ' 5643' month: '06' oa: 1 page: 321 - 336 publication_status: published publisher: Springer publist_id: '1074' pubrep_id: '45' quality_controlled: 0 status: public title: Software transactional memory on relaxed memory models type: conference volume: 5643 year: '2009' ... --- _id: '4385' author: - first_name: Aleksandar full_name: Dragojevic,Aleksandar last_name: Dragojevic - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Anmol full_name: Singh, Anmol V last_name: Singh - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: avoiding conflicts in transactional memories. In: ACM; 2009:7-16. doi:1533' apa: 'Dragojevic, A., Guerraoui, R., Singh, A., & Singh, V. (2009). Preventing versus curing: avoiding conflicts in transactional memories (pp. 7–16). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/1533' chicago: 'Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories,” 7–16. ACM, 2009. https://doi.org/1533.' ieee: 'A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing: avoiding conflicts in transactional memories,” presented at the POPL: Principles of Programming Languages, 2009, pp. 7–16.' ista: 'Dragojevic A, Guerraoui R, Singh A, Singh V. 2009. Preventing versus curing: avoiding conflicts in transactional memories. POPL: Principles of Programming Languages, 7–16.' mla: 'Dragojevic, Aleksandar, et al. Preventing versus Curing: Avoiding Conflicts in Transactional Memories. ACM, 2009, pp. 7–16, doi:1533.' short: A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, ACM, 2009, pp. 7–16. conference: name: 'POPL: Principles of Programming Languages' date_created: 2018-12-11T12:08:35Z date_published: 2009-01-01T00:00:00Z date_updated: 2021-01-12T07:56:34Z day: '01' doi: '1533' extern: 1 month: '01' page: 7 - 16 publication_status: published publisher: ACM publist_id: '1070' quality_controlled: 0 status: public title: 'Preventing versus curing: avoiding conflicts in transactional memories' type: conference year: '2009' ... --- _id: '4384' abstract: - lang: eng text: |- Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system. author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Barbara full_name: Jobstmann, Barbara last_name: Jobstmann - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Guerraoui R, Henzinger TA, Jobstmann B, Singh V. Model checking transactional memories. In: ACM; 2008:372-382. doi:10.1145/1375581.1375626' apa: 'Guerraoui, R., Henzinger, T. A., Jobstmann, B., & Singh, V. (2008). Model checking transactional memories (pp. 372–382). Presented at the PLDI: Programming Languages Design and Implementation, ACM. https://doi.org/10.1145/1375581.1375626' chicago: Guerraoui, Rachid, Thomas A Henzinger, Barbara Jobstmann, and Vasu Singh. “Model Checking Transactional Memories,” 372–82. ACM, 2008. https://doi.org/10.1145/1375581.1375626. ieee: 'R. Guerraoui, T. A. Henzinger, B. Jobstmann, and V. Singh, “Model checking transactional memories,” presented at the PLDI: Programming Languages Design and Implementation, 2008, pp. 372–382.' ista: 'Guerraoui R, Henzinger TA, Jobstmann B, Singh V. 2008. Model checking transactional memories. PLDI: Programming Languages Design and Implementation, 372–382.' mla: Guerraoui, Rachid, et al. Model Checking Transactional Memories. ACM, 2008, pp. 372–82, doi:10.1145/1375581.1375626. short: R. Guerraoui, T.A. Henzinger, B. Jobstmann, V. Singh, in:, ACM, 2008, pp. 372–382. conference: name: 'PLDI: Programming Languages Design and Implementation' date_created: 2018-12-11T12:08:34Z date_published: 2008-01-01T00:00:00Z date_updated: 2021-01-12T07:56:34Z day: '01' doi: 10.1145/1375581.1375626 extern: 1 file: - access_level: open_access checksum: 1238258a27f212fc1a2050a9a246da20 content_type: application/pdf creator: system date_created: 2018-12-12T10:14:05Z date_updated: 2020-07-14T12:46:28Z file_id: '5054' file_name: IST-2012-74-v1+1_Model_checking_transactional_memories.pdf file_size: 201583 relation: main_file file_date_updated: 2020-07-14T12:46:28Z main_file_link: - open_access: '0' url: http://pub.ist.ac.at/%7Etah/Publications/model_checking_transactional_memories.pdf month: '01' oa: 1 page: 372 - 382 publication_status: published publisher: ACM publist_id: '1073' quality_controlled: 0 status: public title: Model checking transactional memories type: conference year: '2008' ... --- _id: '4386' abstract: - lang: eng text: We introduce the notion of permissiveness in transactional memories (TM). Intuitively, a TM is permissive if it never aborts a transaction when it need not. More specifically, a TM is permissive with respect to a safety property p if the TM accepts every history that satisfies p. Permissiveness, like safety and liveness, can be used as a metric to compare TMs. We illustrate that it is impractical to achieve permissiveness deterministically, and then show how randomization can be used to achieve permissiveness efficiently. We introduce Adaptive Validation STM (AVSTM), which is probabilistically permissive with respect to opacity; that is, every opaque history is accepted by AVSTM with positive probability. Moreover, AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms other STMs by up to 40% in read dominated workloads in high contention scenarios. But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness makes AVSTM, on average, 20-30% worse than existing STMs. acknowledgement: This research was supported by the Swiss National Science Foundation. alternative_title: - LNCS author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Guerraoui R, Henzinger TA, Singh V. Permissiveness in transactional memories. In: Vol 5218. Springer; 2008:305-319. doi:10.1007/978-3-540-87779-0_21' apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2008). Permissiveness in transactional memories (Vol. 5218, pp. 305–319). Presented at the DISC: Distributed Computing, Springer. https://doi.org/10.1007/978-3-540-87779-0_21' chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Permissiveness in Transactional Memories,” 5218:305–19. Springer, 2008. https://doi.org/10.1007/978-3-540-87779-0_21. ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Permissiveness in transactional memories,” presented at the DISC: Distributed Computing, 2008, vol. 5218, pp. 305–319.' ista: 'Guerraoui R, Henzinger TA, Singh V. 2008. Permissiveness in transactional memories. DISC: Distributed Computing, LNCS, vol. 5218, 305–319.' mla: Guerraoui, Rachid, et al. Permissiveness in Transactional Memories. Vol. 5218, Springer, 2008, pp. 305–19, doi:10.1007/978-3-540-87779-0_21. short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2008, pp. 305–319. conference: name: 'DISC: Distributed Computing' date_created: 2018-12-11T12:08:35Z date_published: 2008-09-10T00:00:00Z date_updated: 2021-01-12T07:56:35Z day: '10' doi: 10.1007/978-3-540-87779-0_21 extern: 1 intvolume: ' 5218' main_file_link: - open_access: '0' url: http://pub.ist.ac.at/%7Etah/Publications/permissiveness_in_transactional_memories.pdf month: '09' page: 305 - 319 publication_status: published publisher: Springer publist_id: '1072' quality_controlled: 0 status: public title: Permissiveness in transactional memories type: conference volume: 5218 year: '2008' ... --- _id: '4387' abstract: - lang: eng text: Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes. acknowledgement: This research was supported by the Swiss National Science Foundation. alternative_title: - LNCS author: - first_name: Rachid full_name: Guerraoui, Rachid last_name: Guerraoui - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Guerraoui R, Henzinger TA, Singh V. Completeness and nondeterminism in model checking transactional memories. In: Vol 5201. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2008:21-35. doi:10.1007/978-3-540-85361-9_6' apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2008). Completeness and nondeterminism in model checking transactional memories (Vol. 5201, pp. 21–35). Presented at the CONCUR: Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-540-85361-9_6' chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Completeness and Nondeterminism in Model Checking Transactional Memories,” 5201:21–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008. https://doi.org/10.1007/978-3-540-85361-9_6. ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Completeness and nondeterminism in model checking transactional memories,” presented at the CONCUR: Concurrency Theory, 2008, vol. 5201, pp. 21–35.' ista: 'Guerraoui R, Henzinger TA, Singh V. 2008. Completeness and nondeterminism in model checking transactional memories. CONCUR: Concurrency Theory, LNCS, vol. 5201, 21–35.' mla: Guerraoui, Rachid, et al. Completeness and Nondeterminism in Model Checking Transactional Memories. Vol. 5201, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008, pp. 21–35, doi:10.1007/978-3-540-85361-9_6. short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008, pp. 21–35. conference: name: 'CONCUR: Concurrency Theory' date_created: 2018-12-11T12:08:35Z date_published: 2008-07-30T00:00:00Z date_updated: 2021-01-12T07:56:35Z day: '30' doi: 10.1007/978-3-540-85361-9_6 extern: 1 intvolume: ' 5201' main_file_link: - open_access: '0' url: http://pub.ist.ac.at/%7Etah/Publications/completeness_and_nondeterminism_in_model_checking_transactional_memories.pdf month: '07' page: 21 - 35 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '1071' quality_controlled: 0 status: public title: Completeness and nondeterminism in model checking transactional memories type: conference volume: 5201 year: '2008' ... --- _id: '4399' abstract: - lang: eng text: 'A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries. ' acknowledgement: This research was supported in part by the grant SFU/PRG 06-3, and by the Swiss National Science Foundation. alternative_title: - LNCS author: - first_name: Dirk full_name: Beyer, Dirk last_name: Beyer - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Vasu full_name: Vasu Singh id: 4DAE2708-F248-11E8-B48F-1D18A9856A87 last_name: Singh citation: ama: 'Beyer D, Henzinger TA, Singh V. Algorithms for interface synthesis. In: Vol 4590. Springer; 2007:4-19. doi:10.1007/978-3-540-73368-3_4' apa: 'Beyer, D., Henzinger, T. A., & Singh, V. (2007). Algorithms for interface synthesis (Vol. 4590, pp. 4–19). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-540-73368-3_4' chicago: Beyer, Dirk, Thomas A Henzinger, and Vasu Singh. “Algorithms for Interface Synthesis,” 4590:4–19. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_4. ieee: 'D. Beyer, T. A. Henzinger, and V. Singh, “Algorithms for interface synthesis,” presented at the CAV: Computer Aided Verification, 2007, vol. 4590, pp. 4–19.' ista: 'Beyer D, Henzinger TA, Singh V. 2007. Algorithms for interface synthesis. CAV: Computer Aided Verification, LNCS, vol. 4590, 4–19.' mla: Beyer, Dirk, et al. Algorithms for Interface Synthesis. Vol. 4590, Springer, 2007, pp. 4–19, doi:10.1007/978-3-540-73368-3_4. short: D. Beyer, T.A. Henzinger, V. Singh, in:, Springer, 2007, pp. 4–19. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T12:08:39Z date_published: 2007-07-02T00:00:00Z date_updated: 2021-01-12T07:56:41Z day: '02' doi: 10.1007/978-3-540-73368-3_4 extern: 1 intvolume: ' 4590' month: '07' page: 4 - 19 publication_status: published publisher: Springer publist_id: '1059' quality_controlled: 0 status: public title: Algorithms for interface synthesis type: conference volume: 4590 year: '2007' ...