FHPNC '23: "Shape-Constrained Array Programming ..."
Shape-Constrained Array Programming with Size-Dependent Types
Lubin Bailly, Troels Henriksen, and Martin Elsman
(ENS, France; University of Copenhagen, Denmark)
We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.
@InProceedings{FHPNC23p29,
author = {Lubin Bailly and Troels Henriksen and Martin Elsman},
title = {Shape-Constrained Array Programming with Size-Dependent Types},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {29--41},
doi = {10.1145/3609024.3609412},
year = {2023},
}
Publisher's Version
FHPNC '23: "Efficient GPU Implementation ..."
Efficient GPU Implementation of Affine Index Permutations on Arrays
Mathis Bouverot-Dupuis and Mary Sheeran
(ENS Paris, France; Chalmers University of Technology, Sweden)
Optimal usage of the memory system is a key element of fast GPU algorithms. Unfortunately many common algorithms fail in this regard despite exhibiting great regularity in memory access patterns. In this paper we propose efficient kernels to permute the elements of an array. We handle a class of permutations known as Bit Matrix Multiply Complement (BMMC) permutations, for which we design kernels of speed comparable to that of a simple array copy. This is a first step towards implementing a set of array combinators based on these permutations.
@InProceedings{FHPNC23p15,
author = {Mathis Bouverot-Dupuis and Mary Sheeran},
title = {Efficient GPU Implementation of Affine Index Permutations on Arrays},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {15--28},
doi = {10.1145/3609024.3609411},
year = {2023},
}
Publisher's Version
FHPNC '23: "Shape-Constrained Array Programming ..."
Shape-Constrained Array Programming with Size-Dependent Types
Lubin Bailly, Troels Henriksen, and Martin Elsman
(ENS, France; University of Copenhagen, Denmark)
We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.
@InProceedings{FHPNC23p29,
author = {Lubin Bailly and Troels Henriksen and Martin Elsman},
title = {Shape-Constrained Array Programming with Size-Dependent Types},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {29--41},
doi = {10.1145/3609024.3609412},
year = {2023},
}
Publisher's Version
FHPNC '23: "Shape-Constrained Array Programming ..."
Shape-Constrained Array Programming with Size-Dependent Types
Lubin Bailly, Troels Henriksen, and Martin Elsman
(ENS, France; University of Copenhagen, Denmark)
We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.
@InProceedings{FHPNC23p29,
author = {Lubin Bailly and Troels Henriksen and Martin Elsman},
title = {Shape-Constrained Array Programming with Size-Dependent Types},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {29--41},
doi = {10.1145/3609024.3609412},
year = {2023},
}
Publisher's Version
FHPNC '23: "Rank-Polymorphism for Shape-Guided ..."
Rank-Polymorphism for Shape-Guided Blocking
Artjoms Šinkarovs, Thomas Koopman, and Sven-Bodo Scholz
(Heriot-Watt University, UK; Radboud University Nijmegen, Netherlands)
Many numerical algorithms on matrices or tensors can be formulated in a blocking style which improves performance due to better cache locality. In imperative languages, blocking is achieved by introducing additional layers of loops in a nested fashion alongside with suitable adjustments in index computations. While this process is tedious and error-prone, it is also difficult to implement a generically blocked version that would support arbitrary levels of blocking.
At the example of matrix multiply, this paper demonstrates how rank-polymorphic array languages enable the specification of such generically blocked algorithms in a simple, recursive form. The depth of the blocking as well as blocking factors can be encoded in the structure of array shapes. In turn, reshaping arrays makes it possible to switch between blocked and non-blocked arrays. Through rank-polymorphic array combinators, any specification of loop boundaries or explicit index computations can be avoided.
Firstly, we propose a dependently-typed framework for rank-polymorphic arrays. We use it to demonstrate that all blocked algorithms can be naturally derived by induction on the argument shapes. Our framework guarantees lack of out-of-bound indexing, and we also prove that all the blocked versions compute the same results as the canonical algorithm. Secondly, we translate our specification to the array language SaC. Not only do we show that we achieve similar conciseness in the implementation, but we also observe good performance of the generated code. We achieve a 7% improvement compared to the highly-optimised OpenBLAS library, and 3% compared to Intel’s MKL library when running on a 32-core shared-memory system.
@InProceedings{FHPNC23p1,
author = {Artjoms Šinkarovs and Thomas Koopman and Sven-Bodo Scholz},
title = {Rank-Polymorphism for Shape-Guided Blocking},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {1--14},
doi = {10.1145/3609024.3609410},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
FHPNC '23: "Rank-Polymorphism for Shape-Guided ..."
Rank-Polymorphism for Shape-Guided Blocking
Artjoms Šinkarovs, Thomas Koopman, and Sven-Bodo Scholz
(Heriot-Watt University, UK; Radboud University Nijmegen, Netherlands)
Many numerical algorithms on matrices or tensors can be formulated in a blocking style which improves performance due to better cache locality. In imperative languages, blocking is achieved by introducing additional layers of loops in a nested fashion alongside with suitable adjustments in index computations. While this process is tedious and error-prone, it is also difficult to implement a generically blocked version that would support arbitrary levels of blocking.
At the example of matrix multiply, this paper demonstrates how rank-polymorphic array languages enable the specification of such generically blocked algorithms in a simple, recursive form. The depth of the blocking as well as blocking factors can be encoded in the structure of array shapes. In turn, reshaping arrays makes it possible to switch between blocked and non-blocked arrays. Through rank-polymorphic array combinators, any specification of loop boundaries or explicit index computations can be avoided.
Firstly, we propose a dependently-typed framework for rank-polymorphic arrays. We use it to demonstrate that all blocked algorithms can be naturally derived by induction on the argument shapes. Our framework guarantees lack of out-of-bound indexing, and we also prove that all the blocked versions compute the same results as the canonical algorithm. Secondly, we translate our specification to the array language SaC. Not only do we show that we achieve similar conciseness in the implementation, but we also observe good performance of the generated code. We achieve a 7% improvement compared to the highly-optimised OpenBLAS library, and 3% compared to Intel’s MKL library when running on a 32-core shared-memory system.
@InProceedings{FHPNC23p1,
author = {Artjoms Šinkarovs and Thomas Koopman and Sven-Bodo Scholz},
title = {Rank-Polymorphism for Shape-Guided Blocking},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {1--14},
doi = {10.1145/3609024.3609410},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
FHPNC '23: "Efficient GPU Implementation ..."
Efficient GPU Implementation of Affine Index Permutations on Arrays
Mathis Bouverot-Dupuis and Mary Sheeran
(ENS Paris, France; Chalmers University of Technology, Sweden)
Optimal usage of the memory system is a key element of fast GPU algorithms. Unfortunately many common algorithms fail in this regard despite exhibiting great regularity in memory access patterns. In this paper we propose efficient kernels to permute the elements of an array. We handle a class of permutations known as Bit Matrix Multiply Complement (BMMC) permutations, for which we design kernels of speed comparable to that of a simple array copy. This is a first step towards implementing a set of array combinators based on these permutations.
@InProceedings{FHPNC23p15,
author = {Mathis Bouverot-Dupuis and Mary Sheeran},
title = {Efficient GPU Implementation of Affine Index Permutations on Arrays},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {15--28},
doi = {10.1145/3609024.3609411},
year = {2023},
}
Publisher's Version
FHPNC '23: "Rank-Polymorphism for Shape-Guided ..."
Rank-Polymorphism for Shape-Guided Blocking
Artjoms Šinkarovs, Thomas Koopman, and Sven-Bodo Scholz
(Heriot-Watt University, UK; Radboud University Nijmegen, Netherlands)
Many numerical algorithms on matrices or tensors can be formulated in a blocking style which improves performance due to better cache locality. In imperative languages, blocking is achieved by introducing additional layers of loops in a nested fashion alongside with suitable adjustments in index computations. While this process is tedious and error-prone, it is also difficult to implement a generically blocked version that would support arbitrary levels of blocking.
At the example of matrix multiply, this paper demonstrates how rank-polymorphic array languages enable the specification of such generically blocked algorithms in a simple, recursive form. The depth of the blocking as well as blocking factors can be encoded in the structure of array shapes. In turn, reshaping arrays makes it possible to switch between blocked and non-blocked arrays. Through rank-polymorphic array combinators, any specification of loop boundaries or explicit index computations can be avoided.
Firstly, we propose a dependently-typed framework for rank-polymorphic arrays. We use it to demonstrate that all blocked algorithms can be naturally derived by induction on the argument shapes. Our framework guarantees lack of out-of-bound indexing, and we also prove that all the blocked versions compute the same results as the canonical algorithm. Secondly, we translate our specification to the array language SaC. Not only do we show that we achieve similar conciseness in the implementation, but we also observe good performance of the generated code. We achieve a 7% improvement compared to the highly-optimised OpenBLAS library, and 3% compared to Intel’s MKL library when running on a 32-core shared-memory system.
@InProceedings{FHPNC23p1,
author = {Artjoms Šinkarovs and Thomas Koopman and Sven-Bodo Scholz},
title = {Rank-Polymorphism for Shape-Guided Blocking},
booktitle = {Proc.\ FHPNC},
publisher = {ACM},
pages = {1--14},
doi = {10.1145/3609024.3609410},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available