129 lines
11 KiB
BibTeX
129 lines
11 KiB
BibTeX
|
||
@article{woodruff_cheri_2019,
|
||
title = {{CHERI} {Concentrate}: {Practical} {Compressed} {Capabilities}},
|
||
volume = {68},
|
||
copyright = {https://ieeexplore.ieee.org/Xplorehelp/downloads/license-information/IEEE.html},
|
||
issn = {0018-9340, 1557-9956, 2326-3814},
|
||
shorttitle = {{CHERI} {Concentrate}},
|
||
url = {https://ieeexplore.ieee.org/document/8703061/},
|
||
doi = {10.1109/TC.2019.2914037},
|
||
abstract = {We present CHERI Concentrate, a new fat-pointer compression scheme applied to CHERI, the most developed capability-pointer system at present. Capability fat pointers are a primary candidate to enforce fine-grained and non-bypassable security properties in future computer systems, although increased pointer size can severely affect performance. Thus, several proposals for capability compression have been suggested elsewhere that do not support legacy instruction sets, ignore features critical to the existing software base, and also introduce design inefficiencies to RISC-style processor pipelines. CHERI Concentrate improves on the state-of-the-art region-encoding efficiency, solves important pipeline problems, and eases semantic restrictions of compressed encoding, allowing it to protect a full legacy software stack. We present the first quantitative analysis of compiled capability code, which we use to guide the design of the encoding format. We analyze and extend logic from the open-source CHERI prototype processor design on FPGA to demonstrate encoding efficiency, minimize delay of pointer arithmetic, and eliminate additional load-to-use delay. To verify correctness of our proposed high-performance logic, we present a HOL4 machine-checked proof of the decode and pointer-modify operations. Finally, we measure a 50\% to 75\% reduction in L2 misses for many compiled C-language benchmarks running under a commodity operating system using compressed 128-bit and 64-bit formats, demonstrating both compatibility with and increased performance over the uncompressed, 256-bit format.},
|
||
language = {en},
|
||
number = {10},
|
||
urldate = {2024-05-27},
|
||
journal = {IEEE Transactions on Computers},
|
||
author = {Woodruff, Jonathan and Joannou, Alexandre and Xia, Hongyan and Fox, Anthony and Norton, Robert M. and Chisnall, David and Davis, Brooks and Gudka, Khilan and Filardo, Nathaniel W. and Markettos, A. Theodore and Roe, Michael and Neumann, Peter G. and Watson, Robert N. M. and Moore, Simon W.},
|
||
month = oct,
|
||
year = {2019},
|
||
pages = {1455--1469},
|
||
file = {Woodruff et al. - 2019 - CHERI Concentrate Practical Compressed Capabiliti.pdf:/Users/akilan/Zotero/storage/3SZUIWQ5/Woodruff et al. - 2019 - CHERI Concentrate Practical Compressed Capabiliti.pdf:application/pdf},
|
||
}
|
||
|
||
@misc{noauthor_jemalloc_nodate,
|
||
title = {{JEMALLOC}},
|
||
url = {https://jemalloc.net/jemalloc.3.html},
|
||
urldate = {2025-01-15},
|
||
file = {JEMALLOC:/Users/akilan/Zotero/storage/QDEIEJ9N/jemalloc.3.html:text/html},
|
||
}
|
||
|
||
@misc{noauthor_arm_nodate,
|
||
title = {Arm {Architecture} {Reference} {Manual} for {A}-profile architecture},
|
||
url = {https://developer.arm.com/documentation/ddi0487/latest},
|
||
urldate = {2025-01-15},
|
||
file = {Arm Architecture Reference Manual for A-profile architecture:/Users/akilan/Zotero/storage/BVZSP7HA/latest.html:text/html},
|
||
}
|
||
|
||
@misc{noauthor_department_nodate,
|
||
title = {Department of {Computer} {Science} and {Technology} – {CHERI}: {The} {Arm} {Morello} {Board}},
|
||
url = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html},
|
||
urldate = {2025-01-16},
|
||
file = {Department of Computer Science and Technology – CHERI\: The Arm Morello Board:/Users/akilan/Zotero/storage/GCMNX8LY/cheri-morello.html:text/html},
|
||
}
|
||
|
||
@article{navarro_practical_nodate,
|
||
title = {Practical, transparent operating system support for superpages},
|
||
abstract = {Most general-purpose processors provide support for memory pages of large sizes, called superpages. Superpages enable each entry in the translation lookaside buffer (TLB) to map a large physical memory region into a virtual address space. This dramatically increases TLB coverage, reduces TLB misses, and promises performance improvements for many applications. However, supporting superpages poses several challenges to the operating system, in terms of superpage allocation and promotion tradeoffs, fragmentation control, etc. We analyze these issues, and propose the design of an effective superpage management system. We implement it in FreeBSD on the Alpha CPU, and evaluate it on real workloads and benchmarks. We obtain substantial performance benefits, often exceeding 30\%; these benefits are sustained even under stressful workload scenarios.},
|
||
language = {en},
|
||
author = {Navarro, Juan},
|
||
file = {Navarro - Practical, transparent operating system support fo.pdf:/Users/akilan/Zotero/storage/R9MSCWQX/Navarro - Practical, transparent operating system support fo.pdf:application/pdf},
|
||
}
|
||
|
||
@misc{noauthor_ctsrd-cheritoooba_nodate,
|
||
title = {{CTSRD}-{CHERI}/{Toooba}: {RISC}-{V} {Core}; superscalar, out-of-order, multi-core capable; based on {RISCY}-{OOO} from {MIT}},
|
||
url = {https://github.com/CTSRD-CHERI/Toooba},
|
||
urldate = {2025-02-25},
|
||
file = {CTSRD-CHERI/Toooba\: RISC-V Core\; superscalar, out-of-order, multi-core capable\; based on RISCY-OOO from MIT:/Users/akilan/Zotero/storage/BQPSL2D6/Toooba.html:text/html},
|
||
}
|
||
|
||
@article{witaszczyk_pure-capability_nodate,
|
||
title = {Pure-capability third-party software for {Arm} {Morello} and {CHERI}-{RISC}-{V} {CheriBSD}},
|
||
language = {en},
|
||
author = {Witaszczyk, Konrad},
|
||
file = {Witaszczyk - Pure-capability third-party software for Arm Morel.pdf:/Users/akilan/Zotero/storage/549XSPL6/Witaszczyk - Pure-capability third-party software for Arm Morel.pdf:application/pdf},
|
||
}
|
||
|
||
@article{bluespec,
|
||
author = {Nikhil, Rishiyur S. and Arvind},
|
||
title = {What is Bluespec?},
|
||
year = {2008},
|
||
issue_date = {December 2008},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {38},
|
||
number = {23},
|
||
issn = {0163-5743},
|
||
url = {https://doi.org/10.1145/1862867.1862868},
|
||
doi = {10.1145/1862867.1862868},
|
||
abstract = {Bluespec refers to a language and associated tools which are being used for all aspects of hardware system design . specification, synthesis, modeling, and verification. The language, BSV (Bluespec SystemVerilog), is based on a new model of computation for hardware, where all behavior is described as a set of rewrite rules, or Guarded Atomic Actions. Unlike the process/thread model of Verilog, VHDL and SystemC, or the sequential model of C/C++, all behavior of a BSV program can be understood in terms of atomic rule firings. This computational model has a long pedigree in formal specification and verification systems (e.g., Dijkstra's Guarded Commands, UNITY, TLA+, and EventB), and BSV makes it available for hardware design.},
|
||
journal = {SIGDA Newsl.},
|
||
month = dec,
|
||
pages = {1},
|
||
numpages = {1}
|
||
}
|
||
|
||
@incollection{bsv,
|
||
address = {Cham},
|
||
title = {Bluespec {SystemVerilog}},
|
||
isbn = {978-3-319-26408-0},
|
||
url = {https://doi.org/10.1007/978-3-319-26408-0_9},
|
||
abstract = {Bluespec SystemVerilog (BSV) is a rule-based language, where hardware is described as object-oriented modules. Other high-level synthesis approaches try to hide the complexity of hardware (clock cycles, data movement, concurrency, etc.) under the appearance of a sequential and centralized execution. Instead, BSV exposes it to the user as an intuitive high-level metaphor. This language is a good candidate for expert hardware designers with a background on Register-Transfer Level (RTL) languages, such as Verilog or VHDL, for designers that have to develop critical hardware components, or for keeping a very tight control over the performance and the resources used. This chapter introduces the basic concepts of Bluespec SystemVerilog.},
|
||
booktitle = {{FPGAs} for {Software} {Programmers}},
|
||
publisher = {Springer International Publishing},
|
||
author = {Arcas-Abella, Oriol and Sonmez, Nehir},
|
||
editor = {Koch, Dirk and Hannig, Frank and Ziener, Daniel},
|
||
year = {2016},
|
||
doi = {10.1007/978-3-319-26408-0_9},
|
||
pages = {165--172},
|
||
}
|
||
|
||
@inproceedings{Coz,
|
||
author = {Curtsinger, Charlie and Berger, Emery D.},
|
||
title = {Coz: finding code that counts with causal profiling},
|
||
year = {2015},
|
||
isbn = {9781450338349},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
url = {https://doi.org/10.1145/2815400.2815409},
|
||
doi = {10.1145/2815400.2815409},
|
||
abstract = {Improving performance is a central concern for software developers. To locate optimization opportunities, developers rely on software profilers. However, these profilers only report where programs spent their time: optimizing that code may have no impact on performance. Past profilers thus both waste developer time and make it difficult for them to uncover significant optimization opportunities.This paper introduces causal profiling. Unlike past profiling approaches, causal profiling indicates exactly where programmers should focus their optimization efforts, and quantifies their potential impact. Causal profiling works by running performance experiments during program execution. Each experiment calculates the impact of any potential optimization by virtually speeding up code: inserting pauses that slow down all other code running concurrently. The key insight is that this slowdown has the same relative effect as running that line faster, thus "virtually" speeding it up.We present Coz, a causal profiler, which we evaluate on a range of highly-tuned applications: Memcached, SQLite, and the PARSEC benchmark suite. Coz identifies previously unknown optimization opportunities that are both significant and targeted. Guided by Coz, we improve the performance of Memcached by 9\%, SQLite by 25\%, and accelerate six PARSEC applications by as much as 68\%; in most cases, these optimizations involve modifying under 10 lines of code.},
|
||
booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
|
||
pages = {184–197},
|
||
numpages = {14},
|
||
location = {Monterey, California},
|
||
series = {SOSP '15}
|
||
}
|
||
|
||
@article{Toooba, title={Efficient spatial and temporal safety for microcontrollers and application-class processors}, url={https://www.repository.cam.ac.uk/handle/1810/353468}, DOI={10.17863/CAM.99588}, school={Apollo - University of Cambridge Repository}, author={Rugg, Peter}, year={2022}, keywords={CHERI, Hardware design, Memory safety, RISC-V} }
|
||
|
||
@inproceedings {FleetAllocator,
|
||
author = {A.H. Hunter and Chris Kennelly and Paul Turner and Darryl Gove and Tipp Moseley and Parthasarathy Ranganathan},
|
||
title = {Beyond malloc efficiency to fleet efficiency: a hugepage-aware memory allocator},
|
||
booktitle = {15th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 21)},
|
||
year = {2021},
|
||
isbn = {978-1-939133-22-9},
|
||
pages = {257--273},
|
||
url = {https://www.usenix.org/conference/osdi21/presentation/hunter},
|
||
publisher = {{USENIX} Association},
|
||
month = jul
|
||
}
|