Article

Global scheduler properties derived from local restrictions

Authors:

Thomas Arts,

Juan José Sánchez PenasAuthors Info & Claims

ERLANG '02: Proceedings of the 2002 ACM SIGPLAN workshop on Erlang

Pages 49 - 57

https://doi.org/10.1145/592849.592856

Published: 07 October 2002 Publication History

Get Access

Abstract

The VoDka server is a video-on-demand system for a Spanish cable company. We look at the distributed scheduler of this system. This scheduler enables that whenever a user agent is asking for a certain movie, this request is transferred through the system and a set of possible play-back qualities is returned to the agent. In case of a non-empty set, the agent selects one and the movie is streamed to the user.The storage subsystem of the server is composed by a hierarchy of different storage systems, i.e. disks, CD players or tapes. These devices all have restrictions of which the process controlling the device is aware of. A second layer of processes controls a set of devices in one machine and has restrictions, for example, the bandwidth of its connection. A third layer may be further out in the network and serve as a cache to store more popular movies.Every process in the scheduler of the system has a function determining local restrictions, given the configuration and present state of the system. We have built a tool to construct complete models of several configurations. With techniques from the area of formal methods (in particular model checking) these models are used to determine global properties of the system, such as the maximum number of a certain class of movies that can be served in parallel.

References

[1]

J. Armstrong, S. Virding, M. Williams, and C. Wikström. Concurrent Programming in Erlang, 2nd edition. Prentice Hall International, 1996.]]

Digital Library

Google Scholar

[2]

T. Arts and C. Benac Earle. Verifying Erlang code: a resource locker case-study. In Int. Symposium on Formal Methods Europe, volume 2391 of LNCS, pages 183-202. Springer-Verlag, July 2002.]]

Digital Library

Google Scholar

[3]

T. Arts and I. van Langevelde. Correct performance of transaction capabilities. In Int. Conf. on Application of Concurrency to System Design, pages 35-42. IEEE Computer Society Press, June 2001.]]

Digital Library

Google Scholar

[4]

M. Barreiro, V. M. Gulías, J. L. Freire, and J. J. Sánchez. An Erlang-based hierarchical distributed VoD. In 7th Int. Erlang/OTP User Conference (EUC2001). Ericsson Utvecklings AB, September 2001.]]

Google Scholar

[5]

M. Barreiro, V. M. Gulías, J. J. Sánchez, and S. Jorge. The tertiary level in a functional cluster-based hierarchical VoD system. In Functional Programming and λ-Calculus Workshop, volume 2178 of LNCS, pages 540-554. Springer-Verlag, February 2001.]]

Crossref

Google Scholar

[6]

J. Corbett, M. Dwyer, and L. Hatcliff. Bandera: A source-level interface for model checking java programs. In Teaching and Research Demos at ICSE'00, June 2000.]]

Digital Library

Google Scholar

[7]

J. Fernández, H. Garavel, A. Kerbrat, and R. Mateesc. Caesar/Aldébaran development package: A protocol validation and verification toolbox. In 11th Int. Conf. on Computer-Aided Verification, volume 1102 of LNCS, pages 437-440. Springer-Verlag, August 1996.]]

Digital Library

Google Scholar

[8]

J. Groote. The syntax and semantics of timed μCRL. Technical Report SEN-R9709, CWI, Amsterdam, The Netherlands, June 1997.]]

Digital Library

Google Scholar

[9]

J. Groote and B. Lisser. Computer assisted manipulation of algebraic process specifications. Technical Report SEN-R0117, CWI, Amsterdam, The Netherlands, 2001.]]

Digital Library

Google Scholar

[10]

K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. Software Tools for Technology Transfer, 2(4):366-381, March 2000.]]

Crossref

Google Scholar

[11]

G. Holzmann. The Design and Validation of Computer Protocols. Edgewood Cliffs MA: Pretence Hall, 1991.]]

Digital Library

Google Scholar

[12]

ISO/IEC. Lotos --- a formal description technique based on the temporal ordering of observational behaviour. In International Standard 8807, Information Processing Systems --- Open Systems Interconnection. International Organization for Standardization, September 1988.]]

Google Scholar

[13]

SEN group. A language and tool set to study communicating processes with data. Technical report, CWI, http://www.cwi.nl/~mcrl, February 1999.]]

Google Scholar

[14]

A. G. Wouters. Manual for the μCRL tool set (version 2.8.2). Technical Report SEN-R0130, CWI, Amsterdam, The Netherlands, 2001.]]

Google Scholar

Cited By

View all

Fredlund LPenas J(2007)Model checking a video-on-demand server using McErlangProceedings of the 11th international conference on Computer aided systems theory10.5555/1783034.1783108(539-546)Online publication date: 12-Feb-2007
https://dl.acm.org/doi/10.5555/1783034.1783108
Fredlund LSánchez Penas J(2007)Model Checking a Video–on–Demand Server Using McErlangComputer Aided Systems Theory – EUROCAST 200710.1007/978-3-540-75867-9_68(539-546)Online publication date: 2007
https://doi.org/10.1007/978-3-540-75867-9_68
Earle CFredlund LDerrick JSagonas KArmstrong J(2005)Verifying fault-tolerant Erlang programsProceedings of the 2005 ACM SIGPLAN workshop on Erlang10.1145/1088361.1088367(26-34)Online publication date: 26-Sep-2005
https://dl.acm.org/doi/10.1145/1088361.1088367
Show More Cited By

Recommendations

Local proofs for global safety properties

This paper explores locality in proofs of global safety properties of concurrent programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which ...
A Real-Time Disk Scheduler for Multimedia Integrated Server Considering the Disk Internal Scheduler
IPDPS '03: Proceedings of the 17th International Symposium on Parallel and Distributed Processing

The SCSI or the fibre channel (FC) disk drive, called SCSI-FC disk drive has its own internal queue and internal scheduler which maximize its own throughput. The request service order scheduled by the block device drive in Linux is changed by the disk ...
Multimedia Real-Time Disk Scheduling by Hybrid Local/Global Seek-Optimizing Approaches
ICPADS '00: Proceedings of the Seventh International Conference on Parallel and Distributed Systems

Real-time disk scheduling is one of the most important problems in designing a multimedia system. It has been proved to be NP-Complete. In these years, various approaches are proposed to improve disk throughput under guaranteed real-time requirements. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ERLANG '02: Proceedings of the 2002 ACM SIGPLAN workshop on Erlang

October 2002

77 pages

ISBN:1581135920

DOI:10.1145/592849

Conference Chair:
Rex Page
University of Oklahoma
,
Program Chair:
John Hughes
Chalmers Institute of Technology

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 October 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ERLANG02

Sponsor:

SIGPLAN

ERLANG02: Erlang Workshop 2002 ( co-located with ICFP 2002 and PPDP 2002 )

October 7, 2002

Pennsylvania, Pittsburgh

Acceptance Rates

Overall Acceptance Rate 51 of 68 submissions, 75%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
238
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Fredlund LPenas J(2007)Model checking a video-on-demand server using McErlangProceedings of the 11th international conference on Computer aided systems theory10.5555/1783034.1783108(539-546)Online publication date: 12-Feb-2007
https://dl.acm.org/doi/10.5555/1783034.1783108
Fredlund LSánchez Penas J(2007)Model Checking a Video–on–Demand Server Using McErlangComputer Aided Systems Theory – EUROCAST 200710.1007/978-3-540-75867-9_68(539-546)Online publication date: 2007
https://doi.org/10.1007/978-3-540-75867-9_68
Earle CFredlund LDerrick JSagonas KArmstrong J(2005)Verifying fault-tolerant Erlang programsProceedings of the 2005 ACM SIGPLAN workshop on Erlang10.1145/1088361.1088367(26-34)Online publication date: 26-Sep-2005
https://dl.acm.org/doi/10.1145/1088361.1088367
Arts TEarle CSanchez Penas J(2004)Translating Erlang to μCRLProceedings. Fourth International Conference on Application of Concurrency to System Design, 2004. ACSD 2004.10.1109/CSD.2004.1309124(135-144)Online publication date: 2004
https://doi.org/10.1109/CSD.2004.1309124
Penas JRamiro CDäcker BArts T(2003)Extending the VoDKA architecture to improve resource modellingProceedings of the 2003 ACM SIGPLAN workshop on Erlang10.1145/940880.940883(15-22)Online publication date: 29-Aug-2003
https://dl.acm.org/doi/10.1145/940880.940883
Penas JArts T(2003)VoDkaV tool: model checking for extracting global scheduler properties from local restrictionsThird International Conference on Application of Concurrency to System Design, 2003. Proceedings.10.1109/CSD.2003.1207726(247-248)Online publication date: 2003
https://doi.org/10.1109/CSD.2003.1207726
Gulias VAbalde CSanchez J(2002)Lambda Goes to HollywoodPractical Aspects of Declarative Languages10.1007/3-540-36388-2_26(391-407)Online publication date: 16-Dec-2002
https://doi.org/10.1007/3-540-36388-2_26

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Local proofs for global safety properties

A Real-Time Disk Scheduler for Multimedia Integrated Server Considering the Disk Internal Scheduler

Multimedia Real-Time Disk Scheduling by Hybrid Local/Global Seek-Optimizing Approaches