SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 09:40 - 10:00 at SPLASH-I - F-2A Chair(s): Aviral Goel, Reuben Rowe
Fri 20 Nov 2020 21:40 - 22:00 at SPLASH-I - F-2A Chair(s): Pranav Kant, Atsushi Igarashi

Dynamic linking is extremely common in modern software systems,
thanks to the flexibility and space savings it offers.
However, this flexibility comes at a cost:
it's impossible to perform interprocedural optimizations
that involve calls to a dynamic library.
The basic problem is that the run-time behavior of the dynamic linker
can't be predicted at compile time,
so the compiler can make no assumptions about how such calls will behave.

This paper introduces \textit{guided linking},
a technique for optimizing dynamically linked software
when some information about the dynamic linker's behavior is known in advance.
The developer provides an arbitrary set of programs, libraries, and plugins to our tool,
along with \textit{constraints} that limit the possible dynamic linking behavior of the software.
By taking advantage of the constraints, our tool enables
\emph{any} existing optimization to be applied across dynamic linking boundaries.
For example, the NoOverride constraint can be applied to a function
when the developer knows it will never be overridden with a different definition at run time;
guided linking then enables the function to be inlined into its callers in other libraries.
We also introduce a novel code size optimization that
deduplicates identical functions even across different parts of the software set.

By applying guided linking to the Python interpreter and its dynamically loaded modules,
supplying the constraint that no other programs or modules will be used,
we increase speed by an average of 9%.
By applying guided linking to a dynamically linked distribution of Clang and LLVM,
and using the constraint that no other software will use the LLVM libraries,
we can increase speed by 5% and reduce file size by 13%.
If we relax the constraint to allow other software to use the LLVM libraries,
we can still increase speed by 5% and reduce file size by 5%.
If we use guided linking to combine 11 different versions of the Boost library,
using minimal constraints,
we can reduce the total library size by 57%.

Conference Day
Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
F-2AOOPSLA at SPLASH-I +12h
Chair(s): Aviral GoelNortheastern University, Reuben RoweUniversity College London
09:00
20m
Talk
A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
OOPSLA
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
Link to publication DOI Pre-print Media Attached File Attached
09:20
20m
Talk
Resolution as Intersection Subtyping via Modus Ponens
OOPSLA
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
Link to publication DOI Media Attached
09:40
20m
Talk
Guided Linking: Dynamic Linking without the Costs
OOPSLA
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
10:00
20m
Talk
Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
OOPSLA
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Minh-Thai TrinhAdvanced Digital Sciences Center, Nishant RodriguesUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
21:00 - 22:20
F-2AOOPSLA at SPLASH-I
Chair(s): Pranav KantUniversity of Utah, Atsushi IgarashiKyoto University, Japan
21:00
20m
Talk
A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
OOPSLA
Ryan SenanayakeReservoir Labs, Changwan HongMassachusetts Institute of Technology, Ziheng WangMassachusetts Institute of Technology, Amalee WilsonStanford University, Stephen ChouMassachusetts Institute of Technology, Shoaib KamilAdobe Research, Saman AmarasingheMassachusetts Institute of Technology, Fredrik KjolstadStanford University
Link to publication DOI Pre-print Media Attached File Attached
21:20
20m
Talk
Resolution as Intersection Subtyping via Modus Ponens
OOPSLA
Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, Georgios KarachaliasTweag
Link to publication DOI Media Attached
21:40
20m
Talk
Guided Linking: Dynamic Linking without the Costs
OOPSLA
Sean BartellUniversity of Illinois at Urbana-Champaign, Will DietzUniversity of Illinois at Urbana-Champaign, Vikram S. AdveUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached
22:00
20m
Talk
Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
OOPSLA
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Minh-Thai TrinhAdvanced Digital Sciences Center, Nishant RodriguesUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Media Attached