Revise docker permission setup

[PGijsbers]

#495 introduced an issue when building public images: the image is set up for the builder, but the user will start the container under a different uid, which leads to permission errors. I think we should remove any user information from the docker container, and instead create/assign permissions on startup with something like:

set -e

if [ $UID = 0 ]; then
  echo "Docker started as root, not changing file permissions."
  exit 0
fi

user_id=$UID
echo "root" | su -c "adduser --disabled-password --gecos '' -uid $user_id amlb"
echo "root" | su -c "echo '%sudo ALL=(ALL) NOPASSWD:ALL' >> /etc/sudoers"
echo "root" | su -c "chown -R amlb:amlb /home/amlb"
echo "root" | su -c "chown -R amlb:amlb /bench"
echo "root" | su -c "passwd -d amlb"
su "amlb"

And then invoking above script before running python runbenchmark.py.
This way the permissions are set for the person running the docker container, not the one building the image.

Originally posted by @PGijsbers in #495 (comment)