More Like this

1. Resource Allocation Under Sequential Resource Access

   https://doi.org/10.1109/TCOMM.2018.2846657  

   Tajer, Ali; Zohdy, Maha; Alnajjar, Khawla (November 2018, IEEE Transactions on Communications)
2. Resource Deflation: A New Approach For Transient Resource Reclamation

   https://doi.org/10.1145/3302424.3303945  

   Sharma, Prateek; Ali-Eldin, Ahmed; Shenoy, Prashant (March 2019, Proceedings of the Fourteenth EuroSys Conference)

   Data centers and clouds are increasingly offering low-cost computational resources in the form of transient virtual machines. Whenever demand for computational resources exceeds their availability, transient resources can reclaimed by preempting the transient VMs. Conventionally, these transient VMs are used by low-priority applications that can tolerate the disruption caused by preemptions. In this paper we propose an alternative approach for reclaiming resources, called resource deflation. Resource deflation allows applications to dynamically shrink (and expand) in response to resource pressure, instead of being preempted outright. Deflatable VMs allow applications to continue running even under resource pressure, and increase the utility of low-priority transient resources. Deflation uses a dynamic, multi-level cascading reclamation technique that allows applications, operating systems, and hypervisors to implement their own policies for handling resource pressure. For distributed data processing, machine learning, and deep neural network training, our multi-level approach reduces the performance degradation by up to 2x compared to existing preemption-based approaches. When deflatable VMs are deployed on a cluster, our policies allow up to 1.6x utilization without the risk of preemption. 

   more » « less
3. Liquid Resource Types

   Knoth, Tristan; Reynolds, Adam; Wang, Di; Hoffmann, Jan; Polikarpova, Nadia (October 2020, Proceedings of the ACM on programming languages)

   This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility -- automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program's resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof. 

   more » « less
4. Liquid resource types

   https://doi.org/10.1145/3408988  

   Knoth, Tristan; Wang, Di; Reynolds, Adam; Hoffmann, Jan; Polikarpova, Nadia (August 2020, Proceedings of the ACM on Programming Languages)

   This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof. 

   more » « less
5. Towards Effective Resource Procurement in MEC: A Resource Re-Selling Framework

   https://doi.org/10.1109/TSC.2023.3332349  

   Siew, Marie; Sharma, Shikhar; Guo, Kun; Cai, Desmond; Wen, Wanli; Joe-Wong, Carlee; Quek, Tony QS (January 2024, IEEE Transactions on Services Computing)